
neuper@42070: \chapter{Definition der Aufgabenstellung}
neuper@42070: \section{Detaillierte Beschreibung der Aufgabenstellung}
neuper@42070: Zu Beginn des Projekts wurden einige Vorgaben und Ziele des Projektes erarbeitet und im Laufe des Projekts etwas angepasst. Es wurde bewusst auf eine zu einschr\"ankende Aufgabenstellung verzichtet, da Entwicklungen und Erarbeitungen von verschiedenen Umsetzungsstrategien erw\"unscht war. 
neuper@42070: 
neuper@42070: Hauptaugenmerk war dabei auf die Erstellung eines jEdit-Plugins, dass die Verarbeitung von Back's Structured Derivations m\"oglich machen soll, gelegt worden. Mit anderen Worten, es sollte so viel Plugin-Code, wie im begrenzten Projektzeitraum m\"oglich, implementiert werden.
neuper@42070: 
neuper@42070: Weiters sollte eine Projektstruktur aufgebaut werden, die die Initialisierungsarbeiten von weiterf\"uhrende bzw. nachfolgende Projekten erleichtert und somit verk\"urzt. Dabei sollte darauf geachtet werden, dass die vom Isabelleteam bereits verwendete Projekthierarchie soweit wie m\"oglich \"ubernommen bzw. erweitert wird.
neuper@42070: Die nachfolgende Auflistung soll die wichtigsten Tasks nochmals zusammenfassen:
neuper@42070: \begin{enumerate}
neuper@42070: \item Relevante Isabelle Komponenten identifizieren und studieren
neuper@42070: \item Installation der Standard-Komponenten
neuper@42070: \item Entwicklungsumgebung vom Isabelle-Team kopieren
neuper@42070: \item Relevante Komponenten implementieren
neuper@42070:   \begin{itemize}
neuper@42070:   \item jEdit Plugin f\"ur SD
neuper@42070:   \item zugeh\"origen Parser
neuper@42070:   \item nicht vorgesehen: SD-Interpreter in Isar (SML)
neuper@42070:   \end{itemize}
neuper@42070: \end{enumerate}
neuper@42070: 
neuper@42070: \chapter{Beleuchtung der Projekt-relevanten Technologien}
neuper@42070: Dieses Kapitel soll die vielen unterschiedlichen Technologien, die im Rahmen dieser Arbeit verwendet oder zumindest ber\"uhrt wurden, beleuchten und dem Leser helfen, nachfolgende Zusammenh\"ange zu verstehen. Nat\"urlich kann in keines der folgenden Themen sehr tief eingestiegen werden. Viel mehr sollen die nachfolgenden Ausf\"uhrungen einen groben \"Uberblick \"uber die einzelnen Technologien geben.
neuper@42070: \section{Back's Structured Derivations}
neuper@42070: Wie in der Aufgabenstellung bereits beschrieben, war die Erstellung eines Structured Derivation Plugins das Hauptziel dieser Arbeit. Aus diesem Grund wird in diesem Absatz kurz auf die von Prof. Ralph-Johan Back einf\"uhrten Structured Derivations eingegangen und dessen Eigenschaften bzw. Zusammenh\"ange beschrieben.
neuper@42070: 
neuper@42070: Das nachfolgende Beispiel zeigt ein einfaches Beispiel, wie eine Formel mittels SD dargestellt bzw. umgeformt werden kann:
neuper@42070: 
neuper@42070: %{\footnotesize
neuper@42070: \begin{tabbing}
neuper@42070: 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
neuper@42070: \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
neuper@42070: \>  \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
neuper@42070: \>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
neuper@42070: \>  \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
neuper@42070: \>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
neuper@42070: \>  \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
neuper@42070: \>  \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
neuper@42070: \>  \>   \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
neuper@42070: \>  \>$\equiv$\>\vdots\\
neuper@42070: \>  \>  \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
neuper@42070: \>  \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$  \\
neuper@42070: \>  \>     \>$1 + -1 * x$\\
neuper@42070: \>\dots\>$1 + -1 * x$\\
neuper@42070: \>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
neuper@42070: \>  \>$1-x$
neuper@42070: \end{tabbing}
neuper@42070: %}
neuper@42070: 
neuper@42070: Dieses Beispiel kann wie folgt interpretiert werden:
neuper@42070: \begin{enumerate}
neuper@42070: \item Die erste Zeile ist als Angabe bzw. Ausgangspunkt der Berechnung zu verstehen.
neuper@42070: \item Nun folgt der eigentliche Ablauf einer Umformung mittels SD: Mit der Formel in der zweiten Zeile beginnt die Berechnung.
neuper@42070: \item Die n\"achste Zeile gibt nun an, wie die Formel aus der direkt dar\"uberliegenden Zeile umgeformt bzw. aufbereitet wird. Es ist also eine Beschreibung bzw. die passende Rechenregel, um von der Ausgangsformel auf die nachfolgende Formel schlie{\ss}en zu k\"onnen.
neuper@42070: \item Aus dieser Rechenvorschrift ergibt sich die Formel in der n\"achsten Zeile.
neuper@42070: \item Dieser Ablauf wiederholt sich und zieht sich \"uber die weiteren Berechnungen.
neuper@42070: \end{enumerate}
neuper@42070: 
neuper@42070: Back liefert mit SD eine sehr gute Darstellungs- und Verbarbeitungs-Richtlinie, die einerseits dem Leser/Anwender hilft, da durch die Regel- bzw. Beschreibungs-Zeile klar gestellt wird, wie der letzte Berechnungsschritt durchgef\"uhrt wurde. Andererseits bringt SD auch f\"ur den Programmierer einen klaren Vorteil, da \"uber die vorgestellten Sonderzeichen das Parsen von \textit{SD-Code} vereinfacht bzw. direkt (ohne extra Schl\"usselw\"orter einf\"uhren zu m\"ussen) m\"oglich ist.
neuper@42070: 
neuper@42070: \section{Der Texteditor jEdit}\label{jEdit}
neuper@42070: %     http://www.jedit.org/
neuper@42070: %     http://de.wikipedia.org/wiki/JEdit
neuper@42070: %     http://www.chip.de/downloads/jEdit_19235021.html
neuper@42070: %
neuper@42070: jEdit ist ein in Java geschriebener und als Open-Source-Projekt erh\"altlicher Texteditor, der vor allem durch sein sehr gut entwickeltes und ebenso einfaches Plugin-Management-System sehr effektiv eingesetzt 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.
neuper@42070: 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 genannten Gr\"{u}nden nicht zu empfehlen bzw. sinnvoll ist.
neuper@42070: 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.
neuper@42070: 
neuper@42070: \subsection{Das Plugin-System}
neuper@42070: % http://jedit.org/users-guide/writing-plugins-part.html
neuper@42070: 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 anderem die Plugins \textit{Sidekick} und \textit{Konsole} verwendet. Dabei ist es m\"oglich, dass Java-Plugins mit Scala-Plugins kombiniert werden, da diese auch problemlos miteinander kommunizieren k\"{o}nnen.
neuper@42070: 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.
neuper@42070: Weiters bietet sich die M\"oglichkeit, 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. Beim 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.
neuper@42070: 
neuper@42070: 
neuper@42070: \subsection{Pluginstruktur}
neuper@42070: Ein solches jEdit-Plugin muss nat\"{u}rlich ein gewisses 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. 
neuper@42070: 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. 
neuper@42070: 
neuper@42070: \section{Isabelle}
neuper@42070: 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(mit funktionalen sowie imperativen Sprachanteilen). 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 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 Isabelle-Pakete zum Einsatz kommen. Auf diese Pakete soll in den n\"{a}chsten Passagen eingegangen werden.
neuper@42070: 
neuper@42070: \subsection{Isabelle-Pure}
neuper@42070: In diesem Plugin ist der eigentliche CTP-Teil von Isabelle verpackt. Das bedeutet im weiteren Sinn, dass es hier keine grafische Verarbeitung der Daten gibt, sondern der Zugriff von aussen erforderich ist, um den CTP mit Daten zu versorgen und diese nach deren Verabreitung in Isabelle-Pure auszuwerten. Also ist nur hier eine Schnittstelle zum eigentlichen Proofer m\"{o}glich und deshalb ist dieses Plugin f\"{u}r das \sisac-Projekt von zentraler Bedeutung. Standardm\"{a}{\ss}ig ist bereits ein Pure.jar-Paket f\"{u}r jEdit vorhanden. Um SD umsetzten zu k\"{o}nnen, muss hier eine Schnittstelle zu Isabelle-Pure implementiert werden. Nach diesem Schritt kann das Plugin Pure.jar neu gebaut werden. 
neuper@42070: Eine Auflistung der f\"ur das Isabelle-Pure-Packet ben\"otigten Scala-Source-Filles kann Anhang B.2 entnommen werden.
neuper@42070: 
neuper@42070: \subsection{Isabelle-jEdit}
neuper@42070: 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.
neuper@42070: 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 einzelne 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.
neuper@42070: 
neuper@42070: \subsection{Paketstruktur von Isabelle}
neuper@42070: 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.
neuper@42070: Die nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. {\sisac} von Bedeutung sind und und wo diese zu finden sind.
neuper@42070:  
neuper@42070: 
neuper@42070: \begin{itemize}
neuper@42070: \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. 
neuper@42070: \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 werden dieser Ordner und die Pakete erstellt.
neuper@42070: \item \textit{src/Tools/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...} 
neuper@42070: \item \textit{src/Tools/jEditC/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...} Diese beiden obigen Verzeichnisse sind, wie man an der sehr \"{a}hnlichen Pfadstruktur erkennen kann, \"{a}quivalent, wobei der zweite Pfad zum \sisac-Entwicklungsverzeichnis 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.
neuper@42070: \item \textit{src/Tools/jEditC/contrib/jEdit/build/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...} Diesen Aufbau ben\"{o}tigt 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 bzw. sollte dies nur f\"ur schwer nachvollziebare Abl\"aufe ohne Isabelle-Beteiligung angewendet werden. 
neuper@42070: \end{itemize} 
neuper@42070: 
neuper@42070: Siehe dazu auch Anhang B. Dort sind alle relevanten jar-Pakete noch einmal aufgearbeitet und entsprechend gruppiert.
neuper@42070: 
neuper@42070: \section{Die Programmiersprache Scala}
neuper@42070: 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 genauer anzusehen.
neuper@42070: 
neuper@42070: \subsection{Grundlage der Sprache}
neuper@42070: 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 den Vorteilen einer objektorientierten Sprache deckt Scala aber auch die Bed\"{u}rfnisse der funktionalen Programmierung ab. Dies, und vorallem auch das von Erlang \"ubernommene und sehr gut umgesetzte Actorprinzip, sind wohl die Hauptgr\"unde, warum sich das Isabelle-Entwicklungsteam f\"{u}r diese Sprache entschieden hat. Wie bereits erw\"{a}hnt, ist Scala sehr \"{a}hnlich aufgebaut wie Java und hat nebenbei noch den gro{\ss}en Vorteil, dass Scala-Executables in der JVM (Java virtual Machine) ausf\"{u}hrbar sind. Dadurch ist die Plattformunabh\"{a}ngigkeit garantiert und es besteht ein direkter Zusammenhang zwischen Scala und Java der auch bei der jEdit-Plugin-Entwicklung ausgenutzt bzw. verwendet wird.
neuper@42070: 
neuper@42070: Dieser direkte Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing gezeigt bzw. die Vorteile, die daraus resultieren, beleuchtet werden.
neuper@42070: 
neuper@42070: 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 Java-Swing in Scala zu verwenden. Ein JButton(Java) kann zum Beispiel mittels \textit{import javax.swing.JButton} in Scala eingebunden und damit sofort verwendet werden. Auch Scala stellt in seiner Swing-Bibliothek einen Button zur Verf\"{u}gung: \textit{scala.swing.Button}. Es wird nahezu dieselbe Funktionalit\"{a}t angeboten und teilweise die Erzeugung bzw. Verwendung vereinfacht. Man kann sich nun fragen, warum sich die Scala-Entwickler einerseits 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. 
neuper@42070: 
neuper@42070: 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. 
neuper@42070: 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 Konvertierung einer Scala- in eine Java-Komponente n\"{o}tig. Dies kann ganz einfach mittels \textit(peer)-Befehl der Komponente erreicht werden.
neuper@42070: 
neuper@42070: 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.
neuper@42070: 
neuper@42070: \subsection{Scala, Java und jEdit}
neuper@42070: 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. ineinander 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 au\ss ergew\"{o}hnlich und kann bzw. sollte nat\"{u}rlich auch f\"{u}r SD bzw. {\sisac} ausgenutzt werden!
neuper@42070: 
neuper@42070: \subsection{Der Isabelle-Scala-Layer}
neuper@42070: Es sollten nun die Grundlegenden Eigenschaften von Scala bekannt sein. Die Einf\"uhrung des Scala-Layers ab Isabelle-Version 2009 war ein grosser Schritt f\"ur das Isabelle Projekt. Das Scala-Actor-Konzept erm\"oglicht die asynchrone Verarbeitung von einzelnen Beweisteilen und ist einer der massgeblichen Gr\"unde f\"ur die Einf\"uhrung des Scala-Layer. 
neuper@42070: 
neuper@42070: Dieser Absatz sollen nun die Eigenschaften des Scala-Layers und die damit verbundenen Chancen f\"ur das Isac- bzw. SD-Projektes 
neuper@42070: erarbeitet werden. 
neuper@42070: 
neuper@42070: \begin{figure}
neuper@42070: \begin{center}
neuper@42070: \includegraphics[width=100mm]{../fig-reuse-ml-scala-SD}
neuper@42070: \end{center}
neuper@42070: \label{fig-reuse-ml-scala}
neuper@42070: \end{figure}
neuper@42070: 
neuper@42070: Der Scala-Layer verbindet die Java Virtual Maschine (JVM) und den in Standart-ML (SML) geschriebenen Isabelle-Kern. Dabei wird ein internes Protokoll verwendet, dass den Datenaustausch zwischen jEdit und Isabelle/Isar erm\"oglicht. Dieses Protokoll ist im Moment noch (bewusst) ohne API ausgef\"uhrt. Aus diesem Grund musste eine Schnittstelle definiert werden, um den Datenaustausch des SD-Plugins (JVM) mit dem SD-Interpreter m\"oglich zu machen. Siehe dazu den Absatz "Verbindung zum Isabelle-Pure Plugin herstellen". Man kann aus diesem Umstand ableiten, dass die Isabelle-Entwickler mit diesem eingezogenen Scala-Layer und dem damit verbundenen internen Protokoll, auf eine konsistente Verwaltung der Theorie-Bibliotheken abzielen. Mit anderen Worten wird dem Anwendungsprogrammierer der direkte Zugriff auf die Isabelle/Isar-Komponente verwehrt. Der Anwender sollte hier also nicht angreifen sonder die Isabelle-Theorien entsprechend erweitern.
neuper@42070: 
neuper@42070: \chapter{Konfiguration und Implementation der Komponenten}
neuper@42070: Dieses Kapitel soll nun anhand der bereits gewonnen Erkenntnise illustrieren, wie die Entwicklungsumgebung vom Isabelle-Team kopiert wurde und wie wichtigsten Schritte zum SD-Plugin f\"{u}r jEdit wahrscheinlich aussehen werden. Wobei einige Schritte parallel und dadurch nat\"{u}rlich sehr gut im Team umgesetzt werden k\"{o}nnen. Eine genaue Aufstellung aller beteiligten Files k\"onnen dem Anhang D entnommen werden.
neuper@42070: 
neuper@42070: \section{Konfiguration des Netbeans Projektes}
neuper@42070: Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das Netbeans-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert. 
neuper@42070: 
neuper@42070: \begin{enumerate}
neuper@42070: \item Konfigurations-Files von Netbeans in ``Files''-View; beeinflussen sich gegenseitig
neuper@42070:   \begin{enumerate}
neuper@42070:   \item build.xml (aus template erzeugt, keine automatischen Ver\"anderunen)
neuper@42070:   \item nbproject/build-impl.xml (z.T. automatische Ver\"anderunen)
neuper@42070:   \item nbproject/project.xml (z.T. automatische Ver\"anderunen)
neuper@42070:   \item TODO
neuper@42070:   \end{enumerate}
neuper@42070: \item Sacla-plugin installieren laut http://wiki.netbeans.org/Scala69, 
neuper@42070:   \begin{enumerate}
neuper@42070:   \item von ``Install with NetBeasn 6.9''
neuper@42070:   \item nach /usr/local/netbeans.../plugins/scala
neuper@42070:   \end{enumerate}
neuper@42070: \item Scala-plugin installiert in NetBeans
neuper@42070:   \begin{enumerate}
neuper@42070:   \item Men\"u $>$ Tools $>$ Plugins $>$ Downloaded $>$ Add Plugins 
neuper@42070:   \item alle Files von /usr/local/netbeans.../plugins/scala/
neuper@42070:   \item Fenster zeigt alle ausgew\"alten Files
neuper@42070:   \item $<$Install$>$ calls Wizzard $<$Next$>$ probably accept Warning
neuper@42070:   \item Funktionstest: Men\"ue $>$ Files $>$ New Project: zeigt Scala als ``Categories''
neuper@42070:   \end{enumerate}
neuper@42070: \item Neues Projekt ``isac-jedit'' konfigurieren
neuper@42070:   \begin{enumerate}
neuper@42070:   \item Men\"u $>$ Open Project (weil schon aus dem Repository die notwendigen Files vorhanden sind)
neuper@42070:   \item /src/Tools/jeditC: Reference Problems, weil jEdit folgende Plugins braucht
neuper@42070:   \item Funktionskontrolle: ``Projects''-View zeigt das neue Projekt
neuper@42070:   \item Die Konfigurations-Files sind v\"ollig getrennt von anderen Projekten
neuper@42070:   \item Referenz-Probleme beheben; das zeigt auch eventuell fehlende Files
neuper@42070:     \begin{enumerate}
neuper@42070:     \item ``Projects''-View $>$ rightMouse $>$ Resolve Reference Problems: Fenster zeigt dieListe der fehlenden Dateien; $<$Next$>$
neuper@42070:     \item Files holen aus ``Tools'' $>$ Libraries: \"uber Filebrowser aus dem Isabelle\_bundle holen contrib/jEdit---/jars
neuper@42070:     \item ``New Library'' 
neuper@42070:       \begin{enumerate}
neuper@42070:       \item Cobra-renderer: cobra.jar
neuper@42070:       \item Console:  Console.jar
neuper@42070:       \item ErrorList: ErrorList.jar
neuper@42070:       \item Hyperlinks: Hyperlinks.jar
neuper@42070:       \item Isabelle-Pure: Pure.jar
neuper@42070:       \item Rhino-JavaScript: js.jar
neuper@42070:       \item Scala-compiler: scala-compiler.jar
neuper@42070:       \item SideKick: SideKick.jar
neuper@42070:       \end{enumerate}
neuper@42070:     \item Funktions-Kontrollen 
neuper@42070:       \begin{enumerate}
neuper@42070:       \item das kleine gelbe Warndreieck im ``Projects''-View ist verschwunden
neuper@42070:       \item im ``Projects''-View 2 Ordner: ``src'' und ``Libraries''
neuper@42070:       \end{enumerate}
neuper@42070:     \end{enumerate}
neuper@42070:   \item jEdit-Paket zum ``isac-jedit''-Projekt hinzuf\"ugen
neuper@42070:     \begin{enumerate}
neuper@42070:     \item ``Project''-View $>$ rightMouse $>$ Add Jar/Folder: Filebrowser
neuper@42070:     \item /contrib/jedit.../jedit.jar
neuper@42070:     \item Funktions-Kontrolle: ist in ``Projects''/Libraries/jedit.jar
neuper@42070:     \end{enumerate}
neuper@42070:   \item Das neue Projekt ``isac-jedit'' zum Hauptprojekt machen: ``Project''-View $>$ rightMouse $>$ Set as Main Project; Funktions-Kontrolle: der Projektname ist boldface.
neuper@42070:   \end{enumerate}
neuper@42070: \item Ab nun wird die Konfiguration \"uber ``trial and error'' zu Ende gef\"uhrt
neuper@42070:   \begin{enumerate}
neuper@42070:   \item Men\"u $>$ Build Main 
neuper@42070:     \begin{enumerate}
neuper@42070:     \item Wenn: Target ``Isac-impl.jar'' does not exist in the project ``isac-jedit''. It is used from target ``debug''
neuper@42070:       \begin{enumerate}
neuper@42070:       \item Versuch
neuper@42070:         \begin{itemize}
neuper@42070:         \item build-impl.xml l\"oschen
neuper@42070:         \item NetBeans neu starten, stellt build-impl.xml automatisch aus build.xml wieder her
neuper@42070:         \item \dots hat in diesem Fall nicht geholfen
neuper@42070:        \end{itemize}
neuper@42070:       \item Versuch zur Vermutung: Projekt wurde umbenannt von ``Isac'' in ``isac-jedit'', und das machte build.xml inkonsistent
neuper@42070:         \begin{itemize}
neuper@42070:         \item in build.xml query-replace ``Isac'' in ``isac-jedit''
neuper@42070:         \item TODO?
neuper@42070:         \item 
neuper@42070:         \end{itemize}
neuper@42070:       \end{enumerate}
neuper@42070:     \item Wenn: Problem: failed to create tsk or type scalac
neuper@42070:       \begin{enumerate}
neuper@42070:       \item Versuch: Pfad zum Scala bekanntgeben
neuper@42070:         \begin{itemize}
neuper@42070:         \item /usr/local/netbeans-6.9.1/etc/netbeans.conf: netbeans\_default\_options= richtigen Scala-Pfad setzen
neuper@42070:         \item build-impl.xml l\"oschen
neuper@42070:         \item NetBeans neu starten.
neuper@42070:         \end{itemize}
neuper@42070:       \end{enumerate}
neuper@42070:     \item Wenn Fehler: ``/usr/local/isabisac/src/Tools/jEditC/\${project.jEdit}/modes does not exist''
neuper@42070:       \begin{enumerate}
neuper@42070:       \item grep -r "project.jEdit" *
neuper@42070:       \item nbproject/project.properties:project.jEdit=contrib/jEdit
neuper@42070:       \item 
neuper@42070:       \item 
neuper@42070: 
neuper@42070:         \begin{itemize}
neuper@42070:         \item 
neuper@42070:           \begin{itemize}
neuper@42070:           \item 
neuper@42070:           \item 
neuper@42070:           \item 
neuper@42070:           \end{itemize}
neuper@42070:         \item 
neuper@42070:         \item 
neuper@42070:         \end{itemize}
neuper@42070:       \item 
neuper@42070:       \item 
neuper@42070:       \end{enumerate}
neuper@42070:     \item 
neuper@42070:     \item 
neuper@42070:     \end{enumerate}
neuper@42070:   \end{enumerate}
neuper@42070: $<$ $>$
neuper@42070: Men\"u $>$  $>$ $>$  $>$ $>$  $>$
neuper@42070: ``Project''-View $>$ rightMouse $>$ $>$  $>$ $>$  $>$
neuper@42070: \item 
neuper@42070:   \begin{enumerate}
neuper@42070:   \item 
neuper@42070:     \begin{enumerate}
neuper@42070:     \item 
neuper@42070:       \begin{itemize}
neuper@42070:       \item 
neuper@42070:         \begin{itemize}
neuper@42070:         \item 
neuper@42070:         \item 
neuper@42070:         \item 
neuper@42070:         \end{itemize}
neuper@42070:       \item 
neuper@42070:       \item 
neuper@42070:       \end{itemize}
neuper@42070:     \item 
neuper@42070:     \item 
neuper@42070:     \end{enumerate}
neuper@42070:   \item 
neuper@42070:   \item 
neuper@42070:   \end{enumerate}
neuper@42070: \item 
neuper@42070:   \begin{enumerate}
neuper@42070:   \item 
neuper@42070:     \begin{enumerate}
neuper@42070:     \item 
neuper@42070:       \begin{itemize}
neuper@42070:       \item 
neuper@42070:         \begin{itemize}
neuper@42070:         \item 
neuper@42070:         \item 
neuper@42070:         \item 
neuper@42070:         \end{itemize}
neuper@42070:       \item 
neuper@42070:       \item 
neuper@42070:       \end{itemize}
neuper@42070:     \item 
neuper@42070:     \item 
neuper@42070:     \end{enumerate}
neuper@42070:   \item 
neuper@42070:   \item 
neuper@42070:   \end{enumerate}
neuper@42070: \end{enumerate}
neuper@42070: 
neuper@42070: 
neuper@42070: \section{Implementation der jEdit Komponenten}
neuper@42070: 
neuper@42070: \subsection{Erstellen des Plugin-Ger\"{u}sts}
neuper@42070: 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 unter 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. 
neuper@42070: 
neuper@42070: 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 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.
neuper@42070: 
neuper@42070: 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.
neuper@42070: 
neuper@42070: \subsection{Erzeugung des Plugins}
neuper@42070: 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-File erzeugt und danach in den jEdit-Pluginsordner verschoben werden. Die Erzeugung kann nat\"{u}rlich direkt 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 k\"{o}nnen(Ausschnitt aus dem Skript isac\_jedit, Anhang C):
neuper@42070: \begin{enumerate}
neuper@42070: \item Das Plugin kann mittels Kommandline folgenderma{\ss}en erstellt werden: \\ \textit{cd ISABELLE\_HOME/src/Tools/isac/jEdit} $\rightarrow$ \textit{ant jar}
neuper@42070: \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/}
neuper@42070: \item jEdit ausf\"{u}hren und testen
neuper@42070: \end{enumerate}
neuper@42070: 
neuper@42070: \subsection{Verbindung zum Isabelle-Pure Plugin herstellen}
neuper@42070: 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. 
neuper@42070: 
neuper@42070: \begin{figure}
neuper@42070: \begin{center}
neuper@42070: \includegraphics[width=100mm]{../fig-jedit-plugins-SD}
neuper@42070: \end{center}
neuper@42070: \label{fig-jedit-plugins-SD}
neuper@42070: \end{figure}
neuper@42070: 
neuper@42070: Um diesen Schritt setzen 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 hinzugef\"{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.
neuper@42070: 
neuper@42070: 
neuper@42070: \begin{enumerate}
neuper@42070: \item Um den \sisac-Teil im Isabelle-Pure genau abzugrenzen, wurde ein Ordner \textit{Isac} angelegt und ein Testfile \textit{isac.scala} erstellt.
neuper@42070: \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.
neuper@42070: \item Nun kann Pure.jar mittels Kommandline erstellt werden: \textit{cd /src/Pure} $\rightarrow$ \textit{../../bin/isabelle env ./build-jars}
neuper@42070: \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/}
neuper@42070: \item jEdit ausf\"{u}hren und testen
neuper@42070: \end{enumerate}
neuper@42070: Alle die oben angef\"{u}hrten Punkte, sowie das Erzeugen und Kopieren des Plugins selbst, werden vom Script isac\_jedit erledigt.
neuper@42070: Das Skript kann dem Anhang C entnommen werden.
neuper@42070: 
neuper@42070: \section{Umsetzung des SD-Parsers}
neuper@42070: Aus diversen Gr\"{u}nden wurde dieser Punkt im Zuge dieser Projektarbeit nicht mehr umgesetzt sonder nach hinten verschoben. Jedoch gibt es bereits eine Version des Parsers in ML und diese kann in einigen Arbeitsstunden in Zusammenarbeit mit Herrn Neuper in Scala \"{u}bersetzt und eingesetzt werden.
neuper@42070: 
neuper@42070: Es ist bereits ein Parser in ML im Isabelle-Verzeichnis vorhanden, \textit{src/Pure/isar/ parse.ML}. Hier werden sogannte "parse combinators" verwendet. Dasselbe wird in n\"{a}chster Zeit von Seiten des Isabelle-Team auch f\"{u}r den Scala-Parse implementiert. Dadurch lassen sich hieraus auch wichtige Erkenntnisse gewinnen und dies spricht ebenfalls f\"{u}r die Verschiebung dieses Milestones nach hinten. 
neuper@42070: 
neuper@42070: 
neuper@42070: \chapter{Ausblick: Von SD- zum \isac-Plugin}
neuper@42070: 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. 
neuper@42070: 
neuper@42070: 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. 
neuper@42070: 
neuper@42070: \chapter{Zusammenfassung und R\"{u}ckblick}
neuper@42070: Zusammenfassend wird nun ein \"Uberblick gegeben, welche Milestones erledigt wurden und welche nicht; Details dazu finden sich in Anhang A. %TODO
neuper@42070: Abschlie{\ss}end gebe ich einen R\"uckblick auf meine pers\"onlichen Erfahrungen aus dieser Bakkalaureats-Arbeit.
neuper@42070: 
neuper@42070: \section{Zusammenfassung}
neuper@42070: Folgende Milestones wurden erfolgreich abgeschlossen:
neuper@42070: \begin{enumerate}
neuper@42070: \item Relevante Isabelle Komponenten dokumentiert
neuper@42070: 
neuper@42070: \item Installation der Standard-Komponenten:
neuper@42070:   \begin{itemize}
neuper@42070:   \item Mercurial Versioncontrol
neuper@42070:   \item NetBeans IDE
neuper@42070:   \item Standard Isabelle Bundle
neuper@42070:   \end{itemize}
neuper@42070:   
neuper@42070: \item Entwicklungsumgebung vom Isabelle-Team kopieren
neuper@42070:   \begin{itemize}
neuper@42070:   \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
neuper@42070:   \item jEdit als NetBeans Projekt definiert
neuper@42070:   \end{itemize}
neuper@42070:   
neuper@42070: \item Relevante Komponenten implementieren
neuper@42070:   \begin{itemize}
neuper@42070:   \item jEdit Plugin f\"ur SD
neuper@42070:   \item Verbindung des Plugins zu Isabelle
neuper@42070:   \item zugeh\"origen Parser: nur ein Test in SML
neuper@42070:   \end{itemize}
neuper@42070: \end{enumerate}
neuper@42070: 
neuper@42070: \noindent Aus Zeitgr\"unden war {\em nicht} m\"oglich, ein komplettes SD-Plugin zu implementieren; dazu w\"are auch ein Interpreter f\"ur SD auf der ML-Seite n\"otig gewesen.
neuper@42070: 
neuper@42070: \paragraph{Voraussetzungen f\"ur k\"unftige Entwicklung} geschaffen:
neuper@42070: \begin{enumerate}
neuper@42070: \item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
neuper@42070: \item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend
neuper@42070: \item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).
neuper@42070: \end{enumerate}
neuper@42070: 
neuper@42070: \section{R\"uckblick}
neuper@42070: Isabelle ist ein sehr gro\ss es Softwarepacket mit mehreren Millionen LOC. Daher gestaltete sich die Einarbeitungsphase sehr schwierig und kostet sehr viel Zeit. Erschwerend kam hinzu, dass ich von Beginn an mit mehreren, f\"{u}r mich noch ganz neue, Technologien arbeiten musste. Diese Herausforderungen schon zu Beginn machten die Arbeit an \sisac{ }von Beginn an spannend. Hier ist mir vorallem die gemeinsam mit meinem Betreuer Herrn Walther Neuper durchgef\"{u}hrte Installationsarbeit von Isabelle in Erinnerung geblieben. Nie zuvor hatte ich f\"{u}r eine Installation von Software so lange gebraucht - eine ganz neue, wichtige Erfahrung.
neuper@42070: 
neuper@42070: Einer der bedeutensten Milesteine war r\"{u}ckblickend wohl, die Verzeichnisstruktur von Isabelle grunds\"atzlich verstanden zu haben. Bei einem Softwarepacket von dieser Gr\"{o}{\ss}e war es wichtig zu wissen, wo man Files suchen/modifizieren/einf\"{u}gen muss, um den gew\"{u}nschten Effekt erreichen zu k\"onnen.
neuper@42070: 
neuper@42070: Der n\"achste wichtige Schritt war das bereits teilweise bestehende NetBeansprojekt lauff\"ahig zu machen und mir damit zum ersten mal selbst das jEdit-Isabelle-Plugin erzeugen zu k\"onnen. Dies war ein sehr bedeutsamer Schritt, da ich hier zum einen NetBeans und dessen Konfiguration besser kennenlernen konnte und zum anderen sehr viel \"{u}ber die Pluginstruktur eines jEdit-Plugins lernen konnte. Zu Beginn machte mir hier der Mix aus Scala-, Java-, XML- und diversen Config-Files Probleme.
neuper@42070: 
neuper@42070: Bis jetzt hatte ich eigentlich noch nicht wirklich mit der Programmierung des Plugins begonnen doch es waren schon zig Arbeitsstunden rein f\"{u}r Einarbeitungs- und Vorbereitungsaufgaben verstrichen - wieder eine neue Erfahrung f\"{u}r mich. Nach einigen Test- bzw. Beispielprogrammen um die Sprache Scala etwas kennenzulernen, begann die wohl spannenste Phase im Projektverlauf. Das in Java geschriebene Beispielplugin "Quick-Notepad" wurde in Scala \"{u}bersetzt und etwas abge\"andert. 
neuper@42070: 
neuper@42070: Der letzte wirklich bedeutende Schritt war Herstellung der Verbindung zwischen Isabelle-Pure und \sisac. Dieser Punkt ist sehr wichtig, da ohne diese Schnittstelle die Planung des SD-Parser nicht m\"oglich gewesen w\"are. Der letzte Schritt, also die Implementation des SD-Parsers wurde aufgeschoben, da es derzeit seitens des Isabelle-Teams ebenfalls Bestrebungen gibt, einen neuen Scala-Parser zu designen und wir von diesen Erkenntnissen mit Sicherheit in der Zunkft profitieren k\"onnen.
neuper@42070: 
neuper@42070: %Abschlie{\ss}end m\"ochte ich mich bei meinem Betreuer Herrn Walther Neuper sehr herzlich f\"{u}r die gute Betreuung und die spannenden Entwicklungsstuden bedanken. Es war eine sehr lehrreiche und interessante Projektarbeit!
neuper@42070: 
neuper@42070: %\chapter{Milestones und Arbeitsprotokolle}
neuper@42070: %\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010} 
neuper@42070: %\begin{itemize}
neuper@42070: %\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010 
neuper@42070: %\item Charakteristika der Programmsprache Scala: beendet am 27.09.2010
neuper@42070: %\item Scala Actors: beendet am 12.08.2010
neuper@42070: %\end{itemize}
neuper@42070: %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
neuper@42070: %\hline
neuper@42070: %Datum & T\"atigkeit & Einheiten \\ \hline
neuper@42070: %12.07.2010 & Meeting: erste Besprechung und Erkl\"{a}rungen zu Isabelle, Isac und CTPs & 2 \\ \hline
neuper@42070: %15.07.2010 & Recherche \"{u}ber Isabelle und CTPs & 3 \\ \hline
neuper@42070: %20.07.2010 & Meeting: Besprechen der grunds\"{a}tzlichen Vorgangsweise und Ziele & 1 \\ \hline
neuper@42070: %23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline 
neuper@42070: %30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise \"{u}ber Backs 'structured derivations'; Begriffserkl\"{a}rung & 3 \\ \hline
neuper@42070: %01.08.2010 & Recherche: Buch f\"{u}r Scala & 2 \\ \hline
neuper@42070: %03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
neuper@42070: %05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1  \\ \hline
neuper@42070: %06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
neuper@42070: %08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
neuper@42070: %09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
neuper@42070: %12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
neuper@42070: %24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
neuper@42070: %25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
neuper@42070: %27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline \hline
neuper@42070: % & Anzahl der Einheiten & 44 \\
neuper@42070: %\hline
neuper@42070: %\end{tabular}
neuper@42070: %
neuper@42070: %
neuper@42070: %\section{Technische Voraussetzungen hergestellt: beendet am 02.08.2010}
neuper@42070: %\begin{itemize}
neuper@42070: %\item Isabelle installiert, Filestruktur bekannt: beendet am 02.08.2010
neuper@42070: %\item Scala in NetBeans eingebunden: beendet am 22.07.2010
neuper@42070: %\item Mercurial installiert und einrichten des Repositories: beendet am 19.07.2010 
neuper@42070: %\end{itemize}
neuper@42070: %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
neuper@42070: %\hline
neuper@42070: %Datum & T\"atigkeit & Einheiten \\ \hline
neuper@42070: %19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
neuper@42070: %20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
neuper@42070: %21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
neuper@42070: %22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
neuper@42070: %23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline 
neuper@42070: %27.07.2010 & Isabelle-jEdit-Plugin: \"{a}nderungen an der Projektstruktur & 7 \\ \hline
neuper@42070: %28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
neuper@42070: %29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
neuper@42070: %30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung \"{u}ber Erfahrungen mit Filestruktur & 4 \\ \hline
neuper@42070: %02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
neuper@42070: % & Anzahl der Einheiten & 60 \\
neuper@42070: %\hline
neuper@42070: %\end{tabular}
neuper@42070: %
neuper@42070: %\section{NetBeans-Projekt aufgesetzt: beendet am 02.08.2010} 
neuper@42070: %\begin{itemize}
neuper@42070: %\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: beendet am 02.08.2010
neuper@42070: %\item jEdit-Plugin: XML-Files f\"{u}r ISAC vorbereitet: beendet am 22.07.2010
neuper@42070: %\item jEdit-Plugin: Source files geschrieben: beendet am 19.07.2010 
neuper@42070: %\end{itemize}
neuper@42070: %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
neuper@42070: %\hline
neuper@42070: %Datum & T\"atigkeit & Einheiten \\ \hline
neuper@42070: %10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
neuper@42070: %11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
neuper@42070: %21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
neuper@42070: %22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten f\"{u}r ISAC & 3 \\ \hline
neuper@42070: %24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline 
neuper@42070: %26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach L\"{o}sungen & 3 \\ \hline
neuper@42070: %28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
neuper@42070: %29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
neuper@42070: %30.08.2010 & Isabelle-jEdit-Plugin endlich vollst\"{a}ndig lauff\"{a}hig gebracht & 4 \\ \hline
neuper@42070: %01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
neuper@42070: %04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline 
neuper@42070: %20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline 
neuper@42070: %22.09.2010 & Meeting: Fortschrittsbericht, kurze Einf\"{u}hrung f\"{u}r Mitstreiter & 3 \\ \hline
neuper@42070: %
neuper@42070: %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 
neuper@42070: %30.09.2010 & QN: Start mit \"{u}bersetzten der Sourcefiles & 5 \\ \hline
neuper@42070: %02.10.2010 & QN: \"{U}bersetzten der Sourcefiles & 6 \\ \hline
neuper@42070: %04.10.2010 & QN: \"{U}bersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
neuper@42070: %05.10.2010 & QN: QN vollst\"andig in Scala \"{u}bersetzt, testen & 2 \\ \hline \hline
neuper@42070: % & Anzahl der Einheiten & 71 \\
neuper@42070: %\hline
neuper@42070: %\end{tabular}
neuper@42070: %
neuper@42070: %\section{Experimentelle Parser implementiert: beendet am 04.03.2011} 
neuper@42070: %\begin{itemize}
neuper@42070: %\item Experimente mit dem SideKick-Parser abgeschlossen: beendet am 03.02.2011
neuper@42070: %\item Verbindung zu Isabelle-Pure hergestellt: beendet am 04.03.2011
neuper@42070: %\item Implementierung des Scala-Parsers: aufgeschoben
neuper@42070: %\end{itemize}
neuper@42070: %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
neuper@42070: %\hline
neuper@42070: %Datum & T\"atigkeit & Einheiten \\ \hline
neuper@42070: %28.01.2011 & Testen des SideKick-Parsers im Isabelle-Plugin & 2 \\ \hline
neuper@42070: %29.01.2011 & Leichte Modifikationen des SideKick-Parsers im Isabelle-Plugin & 1 \\ \hline
neuper@42070: %08.02.2011 & Besprechung zum Abschluss der praktischen Arbeiten & 1 \\ \hline
neuper@42070: %16.02.2011 & Erstellen des Isabelle-Pur jar-Files & 1 \\ \hline
neuper@42070: %19.02.2011 & Behebung des Problems mit den Umgebungsvariablen & 1 \\ \hline
neuper@42070: %03.03.2011 & Erzeugung des Pure.jar Package m\"{o}glich & 2 \\ \hline
neuper@42070: %04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet  & 3 \\ \hline
neuper@42070: %08.04.2011 & Besprechung: Implementierung des experimentellen Parsers wird nicht mehr durchgef\"{u}hrt & 1 \\ \hline \hline
neuper@42070: % & Anzahl der Einheiten & 12 \\
neuper@42070: %\hline
neuper@42070: %\end{tabular}
neuper@42070: %
neuper@42070: %\section{Verfassen der Dokumentation und abschliesende Arbeiten: beendet am TO.DO.2011}
neuper@42070: %\begin{itemize}
neuper@42070: %\item Bacc.-Protokoll fertiggestellt: beendet am 01.03.2011
neuper@42070: %\item Dokumentation: erste Version fertiggestellt: beendet am 28.04.2011
neuper@42070: %\item Dokumentation abgeschlossen: beendet am TO.DO.2011 
neuper@42070: %\end{itemize}
neuper@42070: %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
neuper@42070: %\hline
neuper@42070: %Datum & T\"atigkeit & Einheiten \\ \hline
neuper@42070: %01.03.2011 & Besprechung zum Ablauf der Dokumentationsarbeiten: Protokoll und Dokumentation & 1 \\ \hline
neuper@42070: %01.03.2011 & Erstellen des Protokolls & 2 \\ \hline
neuper@42070: %08.03.2011 & Besprechung zur Doku und zur Schnittstelle zu Isabelle-Pure & 1 \\ \hline
neuper@42070: %17.03.2011 & Dokumentation schreiben & 2 \\ \hline
neuper@42070: %19.03.2011 & Dokumentation schreiben & 3 \\ \hline
neuper@42070: %24.04.2011 & Dokumentation schreiben & 2 \\ \hline
neuper@42070: %25.04.2011 & Dokumentation schreiben & 4 \\ \hline
neuper@42070: %27.04.2011 & Dokumentation schreiben & 2 \\ \hline
neuper@42070: %28.04.2011 & Dokumentation: Fertigstellen der ersten Version & 3 \\ \hline \hline
neuper@42070: % & Anzahl der Einheiten & 20 \\
neuper@42070: %\hline
neuper@42070: %\end{tabular}
neuper@42070: %
neuper@42070: %\section{Pr\"asentation der Arbeit im IST-Seminar }% am ..(*)...}




