1 \documentclass{article}
6 \bibliographystyle{alpha}
9 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
10 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
11 \def\Problem{ {\tt Problem }}
13 \title{Userinterfaces f\"ur Computer Theorem Prover\\
14 Machbarkeits-Studie im Isac-Projekt
17 \author{Marco Steger\\
18 Bachelorarbeit Telematik\\
19 am Institut f\"ur Softwaretechnologie\\
25 Der Theoremprover Isabelle befindet sich im \"Ubergang von einer Oberfl\"ache f\"ur akademische Benutzer zu einem generellen Frontend, das in verschiedenste softwaretechnische Tools eingebunden werden kann.
27 Die vorliegende Bachelorarbeit in Telematik f\"uhrt in die speziellen, dem k\"unftigen Frontend zugrundleliegenden Konzepte und Komponenten (Scala-Layer f\"ur asynchrone Bearbeitung von Beweisdokumenten, jEdit mit Plugins, Parser) ein, dokumentiert die momentane Organisation dieser Komponenten im Isabelle System und implementiert das gesamte System in einer integrierten Entwicklungsungebung. Diese Implementation entspricht jener des Teils des Isabelle-Teams, das am neuen Frontend arbeitet.
29 Hiermit sind die organisatorischen und softwaretechnische Voraussetzungen daf\"ur geschaffen, dass ein Team an der Technischen Universi\"at Graz an der Entwicklung des kommenden Frontends f\"ur den Theoremprover Isabelle und seiner Integration in Entwicklungswerkzeuge teilhaben kann.
31 %Ziel des Projektes war es, die unz\"{a}hligen M\"{o}glichkeiten, die der Wechsel des Isabelle-Development-Teams vom veralteten Proof General in Verbinung mit dem Editor Emacs auf die neue Scala-Technoligie in Verbindung mit dem Java-Editor jEdit mit sich bringen und wie diese neuen Technologien hier an der TU Graz zum Ausbau des \sisac-Projektes genutzt werden k\"{o}nnen. Um die Weiterentwicklung voranzutreiben, wurden Schnittstellen identifiziert, an denen man an die bereits vorhandene Isabelle-jEdit-Implementierung andocken k\"{o}nnte und welche Vor- und Nachteile die f\"{u}r \sisac mit sich bringen. Weiters wurde der Editor jEdit und vorallem dessen Plugin-Managment-System durchleuchtet und ein Grund-Plugin f\"{u}r die Entwicklung des "structured derivations"-Plugins gelegt. Zuletzt wurde eine Schnittstelle zum Isabelle-Pure-Library implementiert.}
33 \section{Einf\"{u}hrung}\label{intro}
34 Computer Theorem Prover (CTP) sind bis dato in H\"anden eines relativ kleinen Kreises von Experten, von denen der Gro{\ss}teil wiederum im akademischen Bereich arbeitet und nur ein kleiner Teil in der Industrie. Diese Experten bevorzugen Keyboard-Shortcuts (vor Men\"us), reine Texte (ohne mathematische Sonderzeichen) und benutzen auch mit gro{\ss}em Aufwand hergestellte CTP-Entwicklungs-Umgebungen nicht, zum Beispiel die CoqIDE.
36 Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software-Ingenieuren vorzudringen beginnen, stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen.
37 Isabelle stellt sich dieser Herausforderung motiviert durch eine aktuelle technische Entwicklung: Multicore-Maschinen versprechen erh\"ohten Durchsatz, falls Teile von Beweisen parallel abgearbeitet werden k\"onnen. Isabelles Entwurf sieht vor, die Programmsprache Scala (insbesonders seine Actor-Library) als Bindeglied zwischen der Mathematik-Sprache SML und der g\"angisten Plattform f\"ur GUIs vor, der Java-Virtual-Maschine.
39 Die Bachelorarbeit l\"auft im Rahmen des ISAC-Projektes. ISACs experimenteller Mathematik-Assistant baut auf dem SML-Teil von Isabelle auf und es ist geplant, auch sein Frontend in entsprechend geplanten Schritten an die aktuelle Entwicklung von Isabelle anzuschlie{\ss}en. Der erste Schritt geht einen Umweg, um die Technologie kennen zu lernen: Nicht ISACs Rechnungen (mit aufw\"andigen Interaktionen), sondern Backs 'structured derivations' (SD) sollen auf jEdit und Isabelle aufgesetzt werden. Die Bachelorarbeit liefert die Machbarkeits-Studie f\"ur diesen Schritt.
41 \section{Beleuchtung der Projektrelevanten Technologien}
43 \subsection{Der Texteditor jEdit}\label{jEdit}
44 % http://www.jedit.org/
45 % http://de.wikipedia.org/wiki/JEdit
46 % http://www.chip.de/downloads/jEdit_19235021.html
48 jEdit ist ein in Java geschriebener und als Open-Source-Projekt erh\"altlicher Texteditor, der vorallem durch sein sehr gut entwickeltes und ebenso einfaches Plugin-Managment-System sehr effektiv eingetzt werden kann. Solche Plugins k\"{o}nnen direkt in jEdit installiert oder durch manuelles hinzuf\"{u}gen eines Plugin-Paketes genutzt werden. Dadurch ist dieser Editor sehr flexibel in der Anwendung und kann den eigenen Bed\"{u}rfnissen perfekt angepasst werden.
49 Diese Umst\"ande sind wohl auch der Grund, warum sich die Entwickler von Isabelle f\"ur diesen Editor entschieden haben. Hierbei ist zu erw\"{a}hnen, dass hier eine etwas modifizierte bzw. an Isabelle angepasste Version verwendet wird. Es empfiehlt sich daher, immer die aktuelle Version des Isabelle-jEdit-Editors (zB. aus dem Bundle erh\"{a}ltlich auf der Isabelle-Homepage) zu verwenden, da hier diverse Voreinstellungen vorgenommen wurden. In weiterer Folge wird mit jEdit immer diese modifizierte Version des Editors in Verbindung gebracht, da die Verwendung der Grundversion aus oben gennanten Gr\"{u}nden nicht zu empfehlen bzw. sinnvoll ist.
50 Weiters sollte noch erw\"ahnt werden, dass es rund um jEdit einen sehr guten Support via Mailinglist gibt und man wirklich rasch Hilfestellung bekommen kann.
52 \subsubsection{Das Plugin-System}
53 % http://jedit.org/users-guide/writing-plugins-part.html
54 Wie im vorigen Abschnitt bereits erw\"ahnt, ist es sehr einfach und bequem m\"oglich, geeignete Plugins zu installieren bzw. zu verwenden. Es stehen bereits sehr viele verschiedenste Plugins auf der jEdit-Homepage zur Verf\"{u}gung. Diese werden ebenfalls als Open-Source-Projekte angeboten und es bietet sich daher an, bereits verf\"ugbare und funktionierende Plugins als Teil eines neuen Plugins zu verwenden und gegebenenfalls kleine Modifikationen oder Erweiterungen an den Plugins durchzuf\"{u}hren. Im Beispiel von Isabelle wurden unter anderen die Plugins \textit{Sidekick} und \textit{Konsole} verwendent. Dabei ist es m\"oglich, dass Java-Plugins mit Scala-Plugins kombiniert werden und diese k\"{o}nnen auch problemlos miteinander kommunizieren.
55 jEdit bietet einen Plugin-Manager an, mit dem sich sehr einfach bereits installierte Plugins verwalten und updaten lassen und es ist auch m\"{o}glich, neue Plugins direkt zu installieren.
56 Es ist auch m\"{o}glich, selbst implementierte Plugins direkt zu den bereits vorhandenen jEdit-Plugins hizuzuf\"{u}gen. Dazu muss das erzeugte "Plugin".jar Paket ledigich in den jars-Ordner verschoben werden. Dieser OrdnerBeim Start von jEdit wird das neue Plugin automatisch erkannt und hinzugef\"{u}gt. Man muss aber darauf achten, dass \"{a}nderungen nur nach einem Neustart von jEdit \"{u}bernommen werden.
59 \subsubsection{Pluginstruktur}
60 Ein solches jEdit-Plugin muss nat\"{u}rlich einen gewissen Design umsetzen, um von jEdit korrekt ausgef\"{u}hrt werden zu k\"{o}nnen. Grunds\"{a}tzlich besteht ein solches Plugin aus den eigentlichen Sourcefiles und einigen XML- und Property-Datein.
61 Ein m\"{o}glicher Aufbau kann dem Beispiel-Plugin "QuickNotepad"\footnote{http://jedit.org/users-guide/writing-plugins-part.html}, das auf der jEdit-Homepage zu finden ist, entnommen bzw. als Ausgangspunkt f\"{u}r die Entwicklung eines eigenen Plugins herangezogen werden. Weitere Informationen k\"{o}nnen auch dem Paper "Userinterfaces for Computer Theorem Provers" entnommen werden.
64 Isabelle ist einer der f\"{u}hrenden CTPs und an dessen Weiterentwicklung wird st\"{a}ndig gearbeitet. Der letzte gro{\ss}e Schritt betraf den Umstieg von reinem ML auf die Mischsprache Scala. Weiters wurde der in die Jahre gekommene Proof General und der damit in Verbindung stehende Editor Emacs durch den vielseitigen Editor jEdit ersetzt. Dadurch ergeben sich auch f\"{u}r das laufende \sisac-Projekt an der TU Graz neue M\"{o}glichkeiten. Wichtig im Zusammenhang mit dieser Beschreibung ist wichtig zu erw\"{a}hnen, dass hier in weiterer Folge nur noch f\"{u}r jEdit bzw. Scala relevante Teile von Isabelle behandelt und beschrieben werden. Weiters ist wichtig zu wissen, dass f\"{u}r die bereits bestehende Struktur rund um Isablle-jEdit zwei wichtige Isabelle-Pakete zum Einsatz kommen. Auf diese Pakete soll in den n\"{a}chsten Passagen eingegangen werden.
66 \subsubsection{Isabelle-Pure}
67 In diesem Plugin ist der eigentliche CTP-Teil von Isabelle verpackt. Wichtig zu wissen ist, dass es hierzu keine graphische Oberfl\"{a}chen oder direkten zugang von seiten des Editors gibt. Jedoch ist nur hier eine Schnittstelle zum eigentlichen Proofer m\"{o}glich und deshalb f\"{u}r das \sisac-Projekt von zentraler Bedeutung. Stanardm\"{a}{\ss}ig ist bereits ein Pure.jar-Paket f\"{u}r jEdit vorhanden. Um SD umsetzten zu k\"{o}nnen, muss hier einen Schnittstelle zu Isabelle-Pure implementiert werden. Nach diesem Schritt kann das Plugin Pure.jar neu gebaut werden.
69 \subsubsection{Isabelle-jEdit}
70 Dieser Teil von Isabelle repr\"{a}sentiert das Frontend in jEdit. Hier wird also die grafische Aufbereitung der von Isabelle-Pure berechneten Daten \"{u}bernommen. Dieses Plugin zeigt sehr sch\"{o}n, wie bereits bestehende Plugins weiter genutzt und erweitert werden k\"{o}nnen.
71 An diesem Plugin wird von seiten der Isabelle-Entwickler sehr stark weitergearbeitet. Darum sollten hier wohl nicht zu viele, am besten nat\"{u}rlich keine \"{a}nderungen, vorgenommen werden. Der Umstand, dass sich einzellnen Plugins ganz einfach in einem anderen mitverwenden lassen, macht es m\"{o}glich, dass das \sisac-Plugin sehr einfach, im Idealfall von Seiten der Isabelle-Entwickler, in das Isabelle-jEdit-Plugin integriert werden kann.
73 \subsubsection{Paketstruktur von Isabelle}
74 Durch die Komplexit\"{a}t des Isabelle-Entwicklungs-Aufbaus soll hier eine Auflistung aller relevanten jar-Pakete erfolgen. Alle Pakete befinden sich innerhalb der Ordnerstruktur von ISABELLE\_HOME. Darum wird ab hier immer von diesem Verzeichnis ausgegangen.
75 Nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. \sisac von Bedeutung sind und und wo diese zu finden sind.
79 \item \textit{contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, ...} Der Ordner contrib ist in der Repository-Version nicht vorhanden! Dieser kann dem Isabelle-Bundle entnommen werden. Hier befinden sich alle ben\"{o}tigten Zusatztools f\"{u}r Isabelle und darunter eben auch jEdit. In dem oben angef\"{u}hrten Ordner liegen alle Plugins bzw. dorthin werden alle Plugins kopiert, die zusammen mit jEdit gestartet werden sollen. Das oben angef\"{u}hrte Script \"{u}bernimmt genau diesen Kopiervorgang f\"{u}r Isac.jar und Pure.jar.
80 \item \textit{lib/classes:} \textbf{isabelle-scala.jar, pure.jar;} Standardm\"{a}{\ss}ig ist dieser Ordner nicht vorhanden. Erst durch erzeugen der angef\"{u}hrten jar's wird dieser Ordner und die Pakete erstellt.
81 \item \textit{src/Tools/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...}
82 \item \textit{src/Tools/isac/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...} Diese beiden obigen Verzeichnisse sind, wie man an den sehr \"{a}hnlichen Pfadstruktur erkennen kann, \"{a}quivalent wobei der zweite Pfad zum \sisac-Etwicklungsverzeichnis geh\"{o}rt. Hier sind die f\"{u}r das Isabelle-jEdit- bzw. \sisac-Plugin ben\"{o}tigten Plugins und Pakete plus das erzeugte Plugin zu finden.
83 \item \textit{src/Tools/isac/jEdit/contrib/jEdit/build/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...} Diesen Aufbau ben\"{o}tig man nur, wenn man das jEdit-Isac-Projekt direkt in NetBeans debuggen m\"{o}chte. Man erkennt, dass in diesem Verzeichnis der vollst\"{a}ndige Quellcode von jEdit plus allen Plugins, die zusammen mit jEdit gestartet werden sollen, hier zu finden sind. Wie aber bereits erw\"{a}hnt, ist vom direkten Debuggen generell abzuraten.
87 \subsection{Die Programmiersprache Scala}
88 Urspr\"{u}nglich wurde Isabelle rein in ML entwickelt. Erst vor ein paar Jahren wurde mit der \"{U}bersetzung von einigen Teilen in Scala begonnen. Grund genug, sich hier kurz diese neue und sehr vielseitige Sprache etwas anzusehen.
90 \subsubsection{Grundlage der Sprache}
91 Scala ist eine objektorientierte Sprache die sehr \"{a}hnlich zu Java aufgebaut wurde. Dadurch wird die Einarbeitung in diese Programmiersprache f\"{u}r Java-Programmierer sehr vereinfacht. Neben der Vorteilen einer objektorientierten Sprache deckt Scala aber auch die Bed\"{u}rfnisse der funktionalen Programmierung werden mit Scala abgedeckt. Dies ist wohl der Hauptgrund warum sich das Isabelle-Entwicklungsteam f\"{u}r diese Sprache entschieden hat. Wie breits erw\"{a}hnt ist Scala sehr \"{a}hnlich aufgebaut wie Java und hat nebenbei noch den gro{\ss}en Vorteil, das Scala-Executables in der JVM (Java virtual Machine) ausf\"{u}hrbar sind. Dadurch ist die Plattformunabh\"{a}ngigkeit garantiert und es besteht daher ein direkter Zusammenhang zwischen Scala und Java der auch bei der jEdit-Plugin-Entwiklung ausgenutzt bzw. verwedendet wird.
93 Dieser direkte Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing gezeigt bzw. die Vorteile, die daraus resultieren beleuchtet werden.
95 Beide Sprachen stellen diese Grafik-Bibliotheken zur Verf\"{u}gung (und darin auch eigene Shapes und Funktionalit\"{a}t). Es ist jedoch m\"{o}glich, Java-Bibliotheken, wie eben auch Java-Swing in Scala zu verwenden. Ein JButton(Java) kann zum Beispiel mittels \textit{import javax.swing.JButton} in Scala eingebunden und damit sofort auch verwendet werden. Auch Scala stellt in seiner Swing-Bibliothek eine Button zur Verf\"{u}gung: \textit{scala.swing.Button}. Es wird nahezu die selbe Funktionalit\"{a}t angeboten und teilweise die Erzeugung bzw. Verwendung vereinfacht. Man kann sich nun fragen, warum sich die Scala-Entwickler einerseit die M\"{u}he gemacht haben, die Verwendung Java-Swing, wie in Java selbst, m\"{o}glich zu machen und andererseits mit Scala-Swing eine nahezu idente Alternative geschaffen haben.
97 Die Antwort darauf zeigt, wie die Objektorientiertheit von Scala in vielen Bereichen ausgenutzt wurde, um die Sprache mit Funktionalit\"{a}t auszur\"{u}sten, denn es wurde kein neues Konzept f\"{u}r diese Grafikklassen entworfen sondern Wrapper-Objekte/Methoden/Klassen erstellt, die das Arbeiten mit diesen Grafikkomponenten erleichtern soll.
98 Ein Letztes Problem bleibt noch: Es ist zwar sehr einfach ein Java-Swing-Objekt an einen Scala-Swing-Container (zb. Frame) anzubinden, da eine Konvertierung einer Java-Komponente in ein Scala-\"{a}quivalent problemlos m\"{o}glich ist. Jedoch ist oft auch die der Konvertierung einer Scala- in eine Java-Komponente n\"{o}tig. Dies kann ganz einfach mittels \textit(peer)-Befehl der Komponente erreicht werden.
100 Das angef\"{u}hrte Beispiel soll zeigen, wie vielseitig Scala sein kann und welch enormes Potenzial in dieser noch sehr jungen Sprache steckt. Nat\"{u}rlich gibt es dazu eine sehr gut aufgebaute Entwickler-Homepage\footnote{http://www.scala-lang.org/} die Tutorials, Plugin f\"{u}r diverse IDEs und weitere n\"{u}tzliche Hilfestellungen f\"{u}r Scala-Neulinge bereitstellt.
102 \subsubsection{Scala, Java und jEdit}
103 Wie im letzten Abschnitt bereits beschrieben, kommen bei jEdit Java- sowie auch Scala-Komponenten zum Einsatz bzw. werden sogar zu logischen Einheiten kombiniert. So ist zum Beispiel jEdit selbst rein in Java geschrieben und das Plugin Isabelle-jEdit rein in Scala. Trotzdem gibt es \"{u}berhaupt kein Problem diese beiden jar-File miteinander bzw. innereinander in der JVM zu nutzen. Es geht sogar so weit, dass es m\"{o}glich ist, dass das Plugin Isabelle-jEdit bereits vorhandene und rein in Java geschriebene Plugins erweitert und nutzt. Dieses Zusammenspiel zwischen Objekten aus zwei verschiedenen Sprachen ist doch recht aussergew\"{o}hnlich und kann bzw sollte nat\"{u}rlich auch f\"{u}r SD bzw. \sisac ausgenutzt werden!
106 \section{Aufbau des SD-Plugins}
107 Dieses Kapitel soll nun anhand der bereits gewonnen Erkenntnise illustrieren, wie die wichtigsten Schritte zum SD-Plugin f\"{u}r jEdit wahrscheinlich aussehen werden.
108 Wobei einige Schritte parallel und dadurch nat\"{u}rlich sehr gut im Team umgesetzt werden kann.
110 \subsection{Erstellen des Plugin-Ger\"{u}sts}
111 Hier gilt es, erstmal den Umfang der gew\"{u}nschten Anforderungen an das Plugin so genau wie m\"{o}glich zu identifizieren. Hat man eine sehr genaue Vorstellung, wie das GUI des Plugins aussehen wird und welche Zusatz-Features angeboten werden sollen so kann man gezielt untern den bereits bestehenden Plugins f\"{u}r jEdit nach n\"{u}tzlichen Plugins suchen, die in das SD-Plugin (m\"{o}glicherweise durch kleine Modifikationen) integriert werden k\"{o}nnen. Dies spart einerseits sehr viel Zeit und ist nebenbei genau die Art von Programmierung die durch die offnene Plugin-Struktur von jEdit gef\"{o}rdert wird.
113 Hat man nun die Planung abgeschlossen und m\"{o}glicherweise n\"{u}tzliche Plugins gefunden, kann mit der Programmierung des GUIs begonnen werden. Man sollte hier beachten, dass man von Beginn an festlegt, ob mit Scala- oder Java-Swing Komponenten gearbeitet werden soll. Es ist zwar m\"{o}glich, beide Formen zu mischen, doch aus Klarheitsgr\"{u}nden sollte man sich doch f\"{u}r eine Art entscheiden. Wobei hier die Empfehlung im Moment eher noch Richtung Java-Swing geht, da man hier eigentlich f\"{u}r jede Art von Problem bzw. Aufgabe bereits HowTo's im Web finden kann. Da bei Scala-Swing nur Wrapper auf die Java-Swing-Libraries gesetzt wurden, entsteht dadurch auch keinerlei Performance-Verlust.
115 Es existiert bereits ein beispielhaftes Plugin am \sisac-Repository. Da der Grunds\"{a}tzliche Aufbau eines jEdit-Plugins soweit umgesetzt wurde und bereits lauff\"{a}hig ist, sollte man dieses wohl als Ausgangspunkt verwenden. Die direkte Verwendung eines Isabelle-Klons ist wohl zu Beginn nicht zu empfehlen bzw. sollte meiner Meinung nach die Integration von Isac in Isabelle bzw. die Verwachsung der beiden Plugins das Fernziel sein und dadurch w\"{u}rde der Klon-Vorgang wohl eher Probleme schaffen als sie zu l\"{o}sen.
117 \subsection{Erzeugung des Plugins}
118 Hat man die Planung des Plugin-Ger\"{u}sts abgeschlossen und die eigentliche Implementationsphase begonnen, kann dieses Plugin getestet bzw. erzeugt und via jEdit ausgef\"{u}hrt werden. Dazu muss zuerst das jar-Filer erzeugt werden und danach in den jEdit-Pluginsordner verschoben werden. Die Erzeugung kann nat\"{u}rlich dirket mittels NetBeans durchgef\"{u}hrt werden. Doch es ist auch m\"{o}glich dies via Kommandline durchzuf\"{u}hren. Folgende Schritte illustrieren wie die Erzeugung und der Kopiervorgang des Plugins durchgef\"{u}hrt werden kann(Ausschnitt aus dem Skript isac\_jedit):
120 \item Das Plugin kann mittels Kommandline folgenderma{\ss}en erstellt werden: \textit{cd ISABELLE\_HOME/src/Tools/isac/jEdit} $\rightarrow$ \textit{ant jar}
121 \item Nun kann das das neue Plugin ganz einfach kopiert werden \textit{cp contrib/jEdit/build/jars/Isac.jar ../../../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/}
122 \item jEdit ausf\"{u}hren und testen
125 \subsection{Verbindung zum Isabelle-Pure Plugin herstellen}
126 Der n\"{a}chste Schritt sieht nun die Versorgung des GUIs mit Daten vor. Da das jEdit-Plugin selbst nicht rechnen/interpretieren kann, m\"{u}ssen Daten an den Isabelle-Kern, also das Isabelle-Pure-Plugin weitergegeben werden. Dort k\"{o}nnen die Daten verwertet und aufbereitet zur\"{u}ck an das Frontend gereicht werden.
128 Um diesen Schritt setzten zu k\"{o}nnen, muss eine Schnittstelle zwischen dem Kern von Isabelle, Isabelle-Pure und dem Plugin hergestellt werden. Dazu muss zun\"{a}chst Pure.jar leicht modifiziert, danach neu erstellt und zuletzt zu den restlichen jEdit-Plugins hizugef\"{u}gt werden. Dies wurde auf der aktuellen Version am Repository bereits erledigt. Folgende Schritte wurden dazu gesetzt und sind wieder n\"{o}tig, da sicher weitere Modifikationen an der Datei Pure.jar n\"{o}tig sein werden.
131 \item Um den \sisac-Teil im Isabelle-Pure genau abzugrenzen, wurde ein Ordner \textit{Isac} angelegt und ein Testfile \textit{isac.scala} erstellt.
132 \item Nun muss diese File nat\"{u}rlich dem Make-Skript \textit{ISABELLE\_HOME/src/Pure/build-jars} hizugef\"{u}gt werden um beim Erzeugen des jar-Files mitverpackt zu werden.
133 \item Nun kann Pure.jar mittels Kommandline erstellt werden: \textit{cd /src/Pure} $\rightarrow$ \textit{../../bin/isabelle env ./build-jars}
134 \item Nun kann das das neue Plugin ganz einfach kopiert werden \textit{cp ../../lib/classes/Pure.jar ../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/}
135 \item jEdit ausf\"{u}hren und testen
137 Alle die oben angef\"{u}hrten Punkte sowie das Erzeugen und Kopieren des Plugins selbst wird vom Script isac\_jedit erledigt.
139 \subsection{Umseztung des SD-Parsers}
140 Aus Zeitgr\"{u}nden wurde dieser Punkt im Zuge dieser Projektarbeit nicht mehr umgesetzt. Jedoch gibt es bereits eine Version des Parsers in ML und kann in einigen Arbeitsstunden in Zusammenarbeit mit Herrn Neuper in Scala \"{u}bersetzt und eingesetzt werden.
142 \section{Ausblick: Von SD- zum \isac-Plugin}
143 Die obigen Schritte sind n\"{o}tig, um das vorl\"{a}ufige Plugin SD umzusetzen. Nat\"{u}rlich beginnt danach die spannende Arbeit erst so richtig. Ist erst mal ein funktionierender SD-Parser vorhanden, kann dieser immer weiter verbessert und verfeinert werden, bis man auch damit beginnen kann, ihn f\"{u}r das \sisac-Projekt zu nutzen.
145 Daneben kann an der Weiterentwicklung des GUIs gearbeitet werden und die ersten Schritte zur Ann\"{a}herung an das Isabelle-Plugin k\"{o}nnen hier erfolgen.
147 \section{Milestones und Arbeitsprotokolle}
148 \subsection{Inhaltliche Voraussetzungen erarbeitet: am 27.09.2010}
150 \item Kenntnis der Grundlagen und Anwendung von CTP: am 03.08.2010
151 \item Charakteristika der Programmsprache Scala: 27.09.2010
152 \item Scala Actors: am 12.08.2010
154 \begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
156 Datum & T\"atigkeit & Einheiten \\ \hline
157 12.07.2010 & Meeting: erste Besprechung und Erkl\"{a}rungen zu Isabelle, Isac und CTPs & 2 \\ \hline
158 15.07.2010 & Recherche \"{u}ber Isabelle und CTPs & 3 \\ \hline
159 20.07.2010 & Meeting: Besprechen der grunds\"{a}tzlichen Vorgangsweise und Ziele & 1 \\ \hline
160 23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline
161 30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise \"{u}ber Backs 'structured derivations'; Begriffserkl\"{a}rung & 3 \\ \hline
162 01.08.2010 & Recherche: Buch f\"{u}r Scala & 2 \\ \hline
163 03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
164 05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
165 06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
166 08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
167 09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
168 12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
169 24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
170 25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
171 27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline \hline
172 & Anzahl der Einheiten & 44 \\
177 \subsection{Technische Voraussetzungen hergestellt: am 02.08.2010}
179 \item Isabelle installiert, Filestruktur bekannt: am 02.08.2010
180 \item Scala in NetBeans eingebunden: am 22.07.2010
181 \item Mercurial installiert und einrichten des Repositories: 19.07.2010
183 \begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
185 Datum & T\"atigkeit & Einheiten \\ \hline
186 19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
187 20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
188 21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
189 22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
190 23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline
191 27.07.2010 & Isabelle-jEdit-Plugin: \"{a}nderungen an der Projektstruktur & 7 \\ \hline
192 28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
193 29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
194 30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung \"{u}ber Erfahrungen mit Filestruktur & 4 \\ \hline
195 02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
196 & Anzahl der Einheiten & 60 \\
200 \subsection{NetBeans-Projekt aufgesetzt }% am ..(*)...}
202 \item Grundlegende Projektstruktur f\"ur ISAC hergestellt: am 02.08.2010
203 \item jEdit-Plugin: XML-Files f\"{u}r ISAC vorbereitet: am 22.07.2010
204 \item jEdit-Plugin: Source files geschrieben: 19.07.2010
206 \begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
208 Datum & T\"atigkeit & Einheiten \\ \hline
209 10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
210 11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
211 21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
212 22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten f\"{u}r ISAC & 3 \\ \hline
213 24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline
214 26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach L\"{o}sungen & 3 \\ \hline
215 28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
216 29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
217 30.08.2010 & Isabelle-jEdit-Plugin endlich vollst\"{a}ndig lauff\"{a}hig gebracht & 4 \\ \hline
218 01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
219 04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline
220 20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline
221 22.09.2010 & Meeting: Fortschrittsbericht, kurze Einf\"{u}hrung f\"{u}r Mitstreiter & 3 \\ \hline
223 29.09.2010 & Neue Vorgehensweise: QuickNotepad-Plugin(QN) wird in Scala \"{u}bersetzt und f\"{u}r ISAC entsprechend angepasst: Arbeit an den XML-Files & 4 \\ \hline
224 30.09.2010 & QN: Start mit \"{u}bersetzten der Sourcefiles & 5 \\ \hline
225 02.10.2010 & QN: \"{U}bersetzten der Sourcefiles & 6 \\ \hline
226 04.10.2010 & QN: \"{U}bersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
227 05.10.2010 & QN: QN vollständig in Scala \"{u}bersetzt, testen & 2 \\ \hline \hline
228 & Anzahl der Einheiten & 71 \\
232 \subsection{Experimentelle Parser implementiert}% am ..(*)...}
234 \item Experimente mit dem SideKick-Parser abgschlossen: am 03.02.2011
235 \item Verbindung zu Isabelle-Pure hergestellt: am 04.03.2011
236 \item Implementierung des experimentellen Parsers: aus Zeitgr\"{u}nden nicht mehr durchgef\"{u}hrt
238 \begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
240 Datum & T\"atigkeit & Einheiten \\ \hline
241 28.01.2011 & Testen des SideKick-Parsers im Isabelle-Plugin & 2 \\ \hline
242 29.01.2011 & Leichte Modifikationen des SideKick-Parsers im Isabelle-Plugin & 1 \\ \hline
243 08.02.2011 & Besprechung zum Abschluss der praktischen Arbeiten & 1 \\ \hline
244 16.02.2011 & Erstellen des Isabelle-Pur jar-Files & 1 \\ \hline
245 19.02.2011 & Behebung des Problems mit den Umgebungsvariablen & 1 \\ \hline
246 03.03.2011 & Erzeugung des Pure.jar Package m\"{o}glich & 2 \\ \hline
247 04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet & 3 \\ \hline
248 08.04.2011 & Besprechung: Implementierung des experimentellen Parsers wird nicht mehr durchgef\"{u}hrt & 1 \\ \hline \hline
249 & Anzahl der Einheiten & 12 \\
253 \subsection{Verfassen der Dokumentation und abschliesende Arbeiten: am 02.08.2010}
255 \item Bacc.-Protokoll fertiggestellt: am 01.03.2011
256 \item Dokumentation: erste Version fertiggestellt: am 28.04.2011
257 \item Dokumentation abgeschlossen am: TO.DO.2011
259 \begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
261 Datum & T\"atigkeit & Einheiten \\ \hline
262 01.03.2011 & Besprechung zum Ablauf der Dokumentationsarbeiten: Protokoll und Dokumentation & 1 \\ \hline
263 01.03.2011 & Erstellen des Protokolls & 2 \\ \hline
264 08.03.2011 & Besprechung zur Doku und zur Schnittstelle zu Isabelle-Pure & 1 \\ \hline
265 17.03.2011 & Dokumentation schreiben & 2 \\ \hline
266 19.03.2011 & Dokumentation schreiben & 3 \\ \hline
267 24.04.2011 & Dokumentation schreiben & 2 \\ \hline
268 25.04.2011 & Dokumentation schreiben & 4 \\ \hline
269 27.04.2011 & Dokumentation schreiben & 2 \\ \hline
270 28.04.2011 & Dokumentation: Fertigstellen der ersten Version & 3 \\ \hline \hline
271 & Anzahl der Einheiten & 20 \\
275 \subsection{Pr\"asentation der Arbeit im IST-Seminar }% am ..(*)...}
279 %\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}