1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/msteger/bakk-arbeit/CLEANUP Fri Jul 01 10:45:12 2011 +0200
1.3 @@ -0,0 +1,10 @@
1.4 +rm *.dvi
1.5 +rm *.bbl
1.6 +rm *.blg
1.7 +rm *.aux
1.8 +rm *.log
1.9 +rm *.nav
1.10 +rm *.out
1.11 +rm *.snm
1.12 +rm *.toc
1.13 +rm *~
2.1 --- a/doc-src/isac/msteger/bakk-arbeit/content.tex Tue Jun 28 17:09:05 2011 +0200
2.2 +++ b/doc-src/isac/msteger/bakk-arbeit/content.tex Fri Jul 01 10:45:12 2011 +0200
2.3 @@ -1,8 +1,8 @@
2.4 \chapter{Definition der Aufgabenstellung}
2.5 \section{Detaillierte Beschreibung der Aufgabenstellung}
2.6 -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.
2.7 +Zu Beginn des Projekts wurden einige Vorgaben und Ziele des Projektes erarbeitet und im Laufe des Projekts angepasst wo notwendig. Es wurde bewusst auf eine zu einschr\"ankende Aufgabenstellung verzichtet, da Entwicklungen und Erarbeitungen von verschiedenen Umsetzungsstrategien erw\"unscht war.
2.8
2.9 -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.
2.10 +Hauptaugenmerk war dabei auf die Erstellung eines jEdit-Plugins gelegt worden, das als Vorarbeit zu Back's Structured Derivations dienen soll. Mit anderen Worten, es sollte so viel Plugin-Code, wie im begrenzten Projektzeitraum m\"oglich, implementiert werden.
2.11
2.12 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.
2.13 Die nachfolgende Auflistung soll die wichtigsten Tasks nochmals zusammenfassen:
2.14 @@ -11,12 +11,13 @@
2.15 \item Installation der Standard-Komponenten
2.16 \item Entwicklungsumgebung vom Isabelle-Team kopieren
2.17 \item Relevante Komponenten implementieren
2.18 - \begin{itemize}
2.19 - \item jEdit Plugin f\"ur SD
2.20 - \item zugeh\"origen Parser
2.21 - \item nicht vorgesehen: SD-Interpreter in Isar (SML)
2.22 - \end{itemize}
2.23 +\begin{itemize}
2.24 +\item jEdit Plugin f\"ur SD
2.25 +\item zugeh\"origen Parser
2.26 +\item nicht vorgesehen: SD-Interpreter in Isar (SML)
2.27 +\end{itemize}
2.28 \end{enumerate}
2.29 +In Abs.\ref{zusammenfassung} wird r\"uckblickend zusammengefasst, welche dieser Punkte in welchem Ausma\ss{} in dieser Bachelor-Arbeit erledigt wurden.
2.30
2.31 \chapter{Beleuchtung der Projekt-relevanten Technologien}
2.32 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.
2.33 @@ -29,20 +30,20 @@
2.34 \begin{tabbing}
2.35 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
2.36 \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
2.37 -\> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
2.38 +\> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
2.39 \>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
2.40 -\> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
2.41 +\> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
2.42 \>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
2.43 -\> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
2.44 -\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
2.45 -\> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
2.46 -\> \>$\equiv$\>\vdots\\
2.47 -\> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
2.48 -\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
2.49 -\> \> \>$1 + -1 * x$\\
2.50 +\> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
2.51 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
2.52 +\> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
2.53 +\> \>$\equiv$\>\vdots\\
2.54 +\> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
2.55 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
2.56 +\> \> \>$1 + -1 * x$\\
2.57 \>\dots\>$1 + -1 * x$\\
2.58 \>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
2.59 -\> \>$1-x$
2.60 +\> \>$1-x$
2.61 \end{tabbing}
2.62 %}
2.63
2.64 @@ -58,9 +59,9 @@
2.65 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.
2.66
2.67 \section{Der Texteditor jEdit}\label{jEdit}
2.68 -% http://www.jedit.org/
2.69 -% http://de.wikipedia.org/wiki/JEdit
2.70 -% http://www.chip.de/downloads/jEdit_19235021.html
2.71 +% http://www.jedit.org/
2.72 +% http://de.wikipedia.org/wiki/JEdit
2.73 +% http://www.chip.de/downloads/jEdit_19235021.html
2.74 %
2.75 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.
2.76 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.
2.77 @@ -74,14 +75,14 @@
2.78
2.79
2.80 \subsection{Pluginstruktur}
2.81 -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.
2.82 -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.
2.83 +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.
2.84 +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.
2.85
2.86 \section{Isabelle}
2.87 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.
2.88
2.89 \subsection{Isabelle-Pure}
2.90 -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.
2.91 +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.
2.92 Eine Auflistung der f\"ur das Isabelle-Pure-Packet ben\"otigten Scala-Source-Filles kann Anhang B.2 entnommen werden.
2.93
2.94 \subsection{Isabelle-jEdit}
2.95 @@ -91,29 +92,29 @@
2.96 \subsection{Paketstruktur von Isabelle}
2.97 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.
2.98 Die nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. {\sisac} von Bedeutung sind und und wo diese zu finden sind.
2.99 -
2.100 +
2.101
2.102 \begin{itemize}
2.103 -\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.
2.104 +\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.
2.105 \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.
2.106 -\item \textit{src/Tools/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...}
2.107 +\item \textit{src/Tools/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...}
2.108 \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.
2.109 -\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.
2.110 -\end{itemize}
2.111 +\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.
2.112 +\end{itemize}
2.113
2.114 -Siehe dazu auch Anhang B. Dort sind alle relevanten jar-Pakete noch einmal aufgearbeitet und entsprechend gruppiert.
2.115 +Siehe dazu auch Anhang B. Dort sind alle relevanten jar-Pakete noch einmal aufgelistet und entsprechend gruppiert.
2.116
2.117 \section{Die Programmiersprache Scala}
2.118 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.
2.119
2.120 \subsection{Grundlage der Sprache}
2.121 -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.
2.122 +Scala \cite{odersky:scala06} 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 \cite{pl:milner97} ab. Dies, und vorallem auch das von Erlang \cite{armstrong:erlang96} \"ubernommene und sehr gut umgesetzte Actorprinzip \cite{Haller:2009:SAU:1496391.1496422,scala:jmlc06}, 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.
2.123
2.124 Dieser direkte Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing gezeigt bzw. die Vorteile, die daraus resultieren, beleuchtet werden.
2.125
2.126 -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.
2.127 +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.
2.128
2.129 -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.
2.130 +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.
2.131 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.
2.132
2.133 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.
2.134 @@ -122,186 +123,220 @@
2.135 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!
2.136
2.137 \subsection{Der Isabelle-Scala-Layer}
2.138 -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.
2.139 +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.
2.140
2.141 -Dieser Absatz sollen nun die Eigenschaften des Scala-Layers und die damit verbundenen Chancen f\"ur das Isac- bzw. SD-Projektes
2.142 -erarbeitet werden.
2.143 +In diesem Absatz sollen nun die Eigenschaften des Scala-Layers und die damit verbundenen Chancen f\"ur das Isac- bzw. SD-Projektes
2.144 +erarbeitet werden.
2.145
2.146 \begin{figure}
2.147 \begin{center}
2.148 -\includegraphics[width=100mm]{../fig-reuse-ml-scala-SD}
2.149 +\includegraphics[width=100mm]{../fig-reuse-ml-scala-SD.png}
2.150 \end{center}
2.151 \label{fig-reuse-ml-scala}
2.152 +\caption{Der Scala-Layer zwischen Java und SML}
2.153 \end{figure}
2.154
2.155 -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.
2.156 +Wie %Fig.\ref{fig-reuse-ml-scala} WARUM GEHT DAS NICHT ???
2.157 +Fig.3.1
2.158 +zeigt, verbindet der Scala-Layer 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.
2.159
2.160 \chapter{Konfiguration und Implementation der Komponenten}
2.161 -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.
2.162 +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 \ref{files-SD-plugin} entnommen werden.
2.163
2.164 -\section{Konfiguration des Netbeans Projektes}
2.165 -Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das Netbeans-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert.
2.166 +\section{Konfiguration des Netbeans- (NB-) Projektes}
2.167 +Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das NB-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert. Voraussetzung f\"ur die Konfiguration sind die Files aus dem Repository laut Anhang \ref{files-SD-plugin}. Die Konfiguration des NB-Projektes ``testSD-jedit'' erfolgt in folgenden Schritten:
2.168
2.169 \begin{enumerate}
2.170 -\item Konfigurations-Files von Netbeans in ``Files''-View; beeinflussen sich gegenseitig
2.171 +\item Softwarekomponenten aus dem Isabelle\_bundle checken; diese sind alle im Verzeichnis {\tt contrib}:
2.172 \begin{enumerate}
2.173 - \item build.xml (aus template erzeugt, keine automatischen Ver\"anderunen)
2.174 - \item nbproject/build-impl.xml (z.T. automatische Ver\"anderunen)
2.175 - \item nbproject/project.xml (z.T. automatische Ver\"anderunen)
2.176 - \item TODO
2.177 + \item {\tt contrib/scala-\dots} Scala-Compiler und Runtime-System
2.178 + \item {\tt contrib/scala-\dots} jEdit
2.179 + \item {\tt src/Tools/jEditC} der Code f\"ur das Test-Plugin
2.180 \end{enumerate}
2.181 -\item Sacla-plugin installieren laut http://wiki.netbeans.org/Scala69,
2.182 +\item Konfigurations-Files von Netbeans im ``Files''-View checken; Achtung: die Files beeinflussen sich gegenseitig, direkte Eingriffe sind problematisch:
2.183 +\begin{enumerate}
2.184 +\item {\tt build.xml} wurde direkt aus dem Template in {\tt src/Tools/jEdit/} erzeugt; von hier nimmt NB die Daten um Daten in (Teilen von den) anderen Konfigurations-Files zu \"andern; NB nimmt hier keine automatischen Ver\"anderungen vor.
2.185 +\item {\tt nbproject/build-impl.xml} z.T. automatisch erzeugt aus {\tt build.xml} und z.T. untenstehenden Files
2.186 +\item {\tt nbproject/genfiles.properties}
2.187 +\item {\tt nbproject/project.properties}, z.B. Projekt-Name
2.188 +\item {\tt nbproject/project.xml}
2.189 +\end{enumerate}
2.190 +\item Sacla-plugin installieren laut {\tt http://wiki.netbeans.org/Scala69},
2.191 +\begin{enumerate}
2.192 +\item insbesonders siehe ``Install with NetBeans 6.9''
2.193 +\item nach {\tt /usr/local/netbeans.../plugins/scala/} kopieren
2.194 +\end{enumerate}
2.195 +\item Scala-plugin in NB installieren
2.196 +\begin{enumerate}
2.197 +\item Men\"u $>$ Tools $>$ Plugins $>$ Downloaded $>$ Add Plugins
2.198 +\item alle Files von {\tt /usr/local/netbeans\dots/plugins/scala/} ausw\"ahlen
2.199 +\item Fenster in ``Add Plugins'' zeigt alle ausgew\"alten Files
2.200 +\item $<$Install$>$ ruft den Wizzard auf, $<$Next$>$ erzeugt i.A. ein ``Warning'' das zu \"ubergehen ist
2.201 +\item Funktionstest: Men\"ue $>$ Files $>$ New Project: zeigt Scala als ``Categories''
2.202 +\end{enumerate}
2.203 +\item Neues Projekt ``testSD-jedit'' konfigurieren
2.204 +\begin{enumerate}
2.205 +\item Men\"u $>$ Open Project (weil schon aus dem Repository die notwendigen Files vorhanden sind)
2.206 +\item /src/Tools/jeditC: Reference Problems, weil jEdit die Plugins von \ref{plugins} braucht
2.207 +\item Funktionskontrolle: ``Projects''-View zeigt das neue Projekt.\\
2.208 + Die Konfigurations-Files sind v\"ollig getrennt von denen anderer Projekte~!
2.209 +\item\label{reference-pbl} Referenz-Probleme beheben; das zeigt auch eventuell fehlende Files:
2.210 +\begin{enumerate}
2.211 +\item ``Projects''-View $>$ rightMouse $>$ Resolve Reference Problems: Fenster zeigt dieListe der fehlenden Dateien; $<$Next$>$
2.212 +\item Files holen aus ``Tools'' $>$ Libraries: \"uber Filebrowser aus dem Isabelle\_bundle holen {\tt contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars}
2.213 +\item\label{plugins} ``New Library''
2.214 +\begin{enumerate}
2.215 +\item Cobra-renderer: cobra.jar
2.216 +\item Console: Console.jar
2.217 +\item ErrorList: ErrorList.jar
2.218 +\item Hyperlinks: Hyperlinks.jar
2.219 +\item Isabelle-Pure: Pure.jar
2.220 +\item Rhino-JavaScript: js.jar
2.221 +\item Scala-compiler: scala-compiler.jar
2.222 +\item SideKick: SideKick.jar
2.223 +\end{enumerate}
2.224 +\item Funktions-Kontrollen
2.225 +\begin{enumerate}
2.226 +\item das kleine gelbe Warndreieck im ``Projects''-View ist verschwunden
2.227 +\item im ``Projects''-View sind nun 2 Ordner: {\tt src} und {\tt Libraries}
2.228 +\end{enumerate}
2.229 +\end{enumerate}
2.230 +\item jEdit-Paket zum ``testSD-jedit''-Projekt hinzuf\"ugen
2.231 +\begin{enumerate}
2.232 +\item ``Project''-View $>$ rightMouse $>$ Add Jar/Folder: Filebrowser
2.233 +\item /contrib/jedit.../jedit.jar
2.234 +\item Funktions-Kontrolle: ist in ``Projects''/Libraries/jedit.jar
2.235 +\end{enumerate}
2.236 +\item Das neue Projekt ``testSD-jedit'' zum Hauptprojekt machen: ``Project''-View $>$ rightMouse $>$ Set as Main Project; Funktions-Kontrolle: der Projektname ist boldface.
2.237 +\end{enumerate}
2.238 +\item den neuen Isabelle/Scala-Layer ({\tt Pure.jar}) erzeugen mit {\tt bin/testSD}; siehe Pkt.\ref{build-isa-scala} unten.
2.239 +\end{enumerate}
2.240 +
2.241 +\noindent Ab nun wird die Konfiguration \"uber ``trial and error'' zu Ende gef\"uhrt; die unten angef\"uhrten Fehler entstanden durch Umbenennung des Projektes von ``isac-jedit'' auf ``testSD-jedit'' w\"ahrend der oben beschriebenen Installation.
2.242 +\begin{enumerate}
2.243 +\item Build des Plugins schl\"agt fehl: Men\"u $>$ Build Main
2.244 \begin{enumerate}
2.245 - \item von ``Install with NetBeasn 6.9''
2.246 - \item nach /usr/local/netbeans.../plugins/scala
2.247 + \item Fehler: {\it Target ``Isac-impl.jar'' does not exist in the project ``testSD-jedit''. It is used from target ``debug''}
2.248 + \begin{enumerate}
2.249 + \item\label{restart-NB} Versuch
2.250 + \begin{itemize}
2.251 + \item {\tt build-impl.xml} l\"oschen
2.252 + \item NetBeans neu starten, stellt build-impl.xml automatisch aus build.xml wieder her
2.253 + \item \dots hat in diesem Fall nicht geholfen
2.254 + \end{itemize}
2.255 + \item Versuch zur Vermutung: Projekt wurde umbenannt von ``Isac'' in ``testSD-jedit'', entsprechende Eintr\"age in den Konfigurations-Dateien wurden automatisch richtig ersetzt, aber nicht in {\tt build.xml}
2.256 + \begin{itemize}
2.257 + \item in {\tt build.xml} query-replace ``isac-jedit'' in ``testSD-jedit''
2.258 + \end{itemize}
2.259 + \end{enumerate}
2.260 + \item Fehler: {\it Problem: failed to create task or type scalac}
2.261 + \begin{enumerate}
2.262 + \item Versuch: Pfad zum Scala bekanntgeben
2.263 + \begin{itemize}
2.264 + \item {\tt /usr/local/netbeans-6.9.1/etc/netbeans.conf}: netbeans\_default\_options= \dots richtigen Scala-Pfad setzen
2.265 + \item build-impl.xml l\"oschen
2.266 + \item NetBeans neu starten (siehe \ref{restart-NB}).
2.267 + \end{itemize}
2.268 + \end{enumerate}
2.269 + \item Wenn Fehler: {\it /usr/local/isabisac/src/Tools/jEditC/\${project.jEdit}/modes does not exist}
2.270 + \begin{enumerate}
2.271 + \item grep -r "project.jEdit" *
2.272 + \item {\tt nbproject/project.properties}: project.jEdit=contrib/jEdit
2.273 \end{enumerate}
2.274 -\item Scala-plugin installiert in NetBeans
2.275 + \end{enumerate}%??indent
2.276 +\item Fehlersuche in den Project Files, nicht in {\tt build.xml}:\\
2.277 +{\it src/Tools/jEditC/src/testSD.scala:225: error: value Isac is not a member of package isabelle}
2.278 \begin{enumerate}
2.279 - \item Men\"u $>$ Tools $>$ Plugins $>$ Downloaded $>$ Add Plugins
2.280 - \item alle Files von /usr/local/netbeans.../plugins/scala/
2.281 - \item Fenster zeigt alle ausgew\"alten Files
2.282 - \item $<$Install$>$ calls Wizzard $<$Next$>$ probably accept Warning
2.283 - \item Funktionstest: Men\"ue $>$ Files $>$ New Project: zeigt Scala als ``Categories''
2.284 + \item den Link zu {\tt testSD.scala:22} folgen
2.285 + \item\label{build-intermed} als Zwischenschritt eine noch nicht erzeugte Class ``Isac'' auskommentieren; siehe Pkt.\ref{build-intermed-end} unten\\
2.286 +val str1: String = isabelle.Isac.parse(``Testdaten aus dem Parser!'')\\
2.287 + val str1: String = ``TEST'' //isabelle.Isac.parse(``Testdaten aus dem Parser!'')
2.288 + \item nochmals Men\"u $>$ Build (Hammer) \dots successful (wegen auskommentierter Zeile)
2.289 + \item in der Konsole beobachten, welche Files kopiert werden und vergleichen mit {\tt build.xml}, z.B.
2.290 + $<$target name=''-pre-jar''$>$
2.291 + $<$target name=''-post-jar''$>$
2.292 + \item {\tt bin/testSD} ausf\"uhren \dots
2.293 + \item =dots stellt den entscheidender Schritt dar: ein neues {\tt Pure.jar} wurde erzeugt; dieses ist nun erweitert mit einer class {\tt Isac}; diese Klasse wurde erzeugt durch Code in \\{\tt scr/Pure/Isac/isac.scala}
2.294 + \item\label{build-intermed-end} den Zwischenschritt Pkt.\ref{build-intermed} oben r\"uckg\"angig machen:\\
2.295 + ``val str1: String = isabelle.Isac.parse(``Testdaten aus dem Parser!'')".\\
2.296 + Dieser Befehl braucht das {\em neue} {\tt Pure.jar} am richtigen Platz \dots
2.297 + \item \dots das Shellscript {\tt bin/testSD\_jedit} erzeugt dieses {\tt Pure.jar}
2.298 \end{enumerate}
2.299 -\item Neues Projekt ``isac-jedit'' konfigurieren
2.300 +\item\label{build-isa-scala} Fehler beim Exekutieren von {\tt bin/testSD}
2.301 \begin{enumerate}
2.302 - \item Men\"u $>$ Open Project (weil schon aus dem Repository die notwendigen Files vorhanden sind)
2.303 - \item /src/Tools/jeditC: Reference Problems, weil jEdit folgende Plugins braucht
2.304 - \item Funktionskontrolle: ``Projects''-View zeigt das neue Projekt
2.305 - \item Die Konfigurations-Files sind v\"ollig getrennt von anderen Projekten
2.306 - \item Referenz-Probleme beheben; das zeigt auch eventuell fehlende Files
2.307 - \begin{enumerate}
2.308 - \item ``Projects''-View $>$ rightMouse $>$ Resolve Reference Problems: Fenster zeigt dieListe der fehlenden Dateien; $<$Next$>$
2.309 - \item Files holen aus ``Tools'' $>$ Libraries: \"uber Filebrowser aus dem Isabelle\_bundle holen contrib/jEdit---/jars
2.310 - \item ``New Library''
2.311 - \begin{enumerate}
2.312 - \item Cobra-renderer: cobra.jar
2.313 - \item Console: Console.jar
2.314 - \item ErrorList: ErrorList.jar
2.315 - \item Hyperlinks: Hyperlinks.jar
2.316 - \item Isabelle-Pure: Pure.jar
2.317 - \item Rhino-JavaScript: js.jar
2.318 - \item Scala-compiler: scala-compiler.jar
2.319 - \item SideKick: SideKick.jar
2.320 - \end{enumerate}
2.321 - \item Funktions-Kontrollen
2.322 - \begin{enumerate}
2.323 - \item das kleine gelbe Warndreieck im ``Projects''-View ist verschwunden
2.324 - \item im ``Projects''-View 2 Ordner: ``src'' und ``Libraries''
2.325 - \end{enumerate}
2.326 - \end{enumerate}
2.327 - \item jEdit-Paket zum ``isac-jedit''-Projekt hinzuf\"ugen
2.328 - \begin{enumerate}
2.329 - \item ``Project''-View $>$ rightMouse $>$ Add Jar/Folder: Filebrowser
2.330 - \item /contrib/jedit.../jedit.jar
2.331 - \item Funktions-Kontrolle: ist in ``Projects''/Libraries/jedit.jar
2.332 - \end{enumerate}
2.333 - \item Das neue Projekt ``isac-jedit'' zum Hauptprojekt machen: ``Project''-View $>$ rightMouse $>$ Set as Main Project; Funktions-Kontrolle: der Projektname ist boldface.
2.334 + \item einfach auf die ``error messages'' schauen, eg. {\it src/Pure/: no such file or directory} \dots
2.335 + \item \dots hei\ss t, dass das Skript nicht vom richtigen Pfad {\tt \~{\,}\~{\,}} gestartet wurde --- dieses Skript sollte also verbessert werden.
2.336 + \item Funktionstest: \\
2.337 + \#\#\#\\
2.338 + \#\#\# Building Isabelle/Scala layer\\
2.339 + \#\#\#
2.340 \end{enumerate}
2.341 -\item Ab nun wird die Konfiguration \"uber ``trial and error'' zu Ende gef\"uhrt
2.342 - \begin{enumerate}
2.343 - \item Men\"u $>$ Build Main
2.344 - \begin{enumerate}
2.345 - \item Wenn: Target ``Isac-impl.jar'' does not exist in the project ``isac-jedit''. It is used from target ``debug''
2.346 - \begin{enumerate}
2.347 - \item Versuch
2.348 - \begin{itemize}
2.349 - \item build-impl.xml l\"oschen
2.350 - \item NetBeans neu starten, stellt build-impl.xml automatisch aus build.xml wieder her
2.351 - \item \dots hat in diesem Fall nicht geholfen
2.352 - \end{itemize}
2.353 - \item Versuch zur Vermutung: Projekt wurde umbenannt von ``Isac'' in ``isac-jedit'', und das machte build.xml inkonsistent
2.354 - \begin{itemize}
2.355 - \item in build.xml query-replace ``Isac'' in ``isac-jedit''
2.356 - \item TODO?
2.357 - \item
2.358 - \end{itemize}
2.359 - \end{enumerate}
2.360 - \item Wenn: Problem: failed to create tsk or type scalac
2.361 - \begin{enumerate}
2.362 - \item Versuch: Pfad zum Scala bekanntgeben
2.363 - \begin{itemize}
2.364 - \item /usr/local/netbeans-6.9.1/etc/netbeans.conf: netbeans\_default\_options= richtigen Scala-Pfad setzen
2.365 - \item build-impl.xml l\"oschen
2.366 - \item NetBeans neu starten.
2.367 - \end{itemize}
2.368 - \end{enumerate}
2.369 - \item Wenn Fehler: ``/usr/local/isabisac/src/Tools/jEditC/\${project.jEdit}/modes does not exist''
2.370 - \begin{enumerate}
2.371 - \item grep -r "project.jEdit" *
2.372 - \item nbproject/project.properties:project.jEdit=contrib/jEdit
2.373 - \item
2.374 - \item
2.375 +\item Fehlermeldung beim Starten des Plugins aus NB, die \"ubergehen sind:
2.376 +\begin{verbatim}
2.377 +/home/neuper/.jedit/jars/Console.jar:
2.378 +Two copies installed. Please remove one of the two copies.
2.379 +/home/neuper/.jedit/jars/Hyperlinks.jar:
2.380 +Two copies installed. Please remove one of the two copies.
2.381 +/home/neuper/.jedit/jars/SideKick.jar:
2.382 +Two copies installed. Please remove one of the two copies.
2.383 +/home/neuper/.jedit/jars/ErrorList.jar:
2.384 +Two copies installed. Please remove one of the two copies.
2.385 +\end{verbatim}
2.386 +Fehler zu beseitigen mit {\tt rm -r \~/jedit/jars}
2.387 +\item \textit{Referenzproblem} auf {\tt Pure.jar}: siehe Pkt.\ref{reference-pbl} auf S.\pageref{reference-pbl}.
2.388
2.389 - \begin{itemize}
2.390 - \item
2.391 - \begin{itemize}
2.392 - \item
2.393 - \item
2.394 - \item
2.395 - \end{itemize}
2.396 - \item
2.397 - \item
2.398 - \end{itemize}
2.399 - \item
2.400 - \item
2.401 - \end{enumerate}
2.402 - \item
2.403 - \item
2.404 - \end{enumerate}
2.405 - \end{enumerate}
2.406 -$<$ $>$
2.407 -Men\"u $>$ $>$ $>$ $>$ $>$ $>$
2.408 -``Project''-View $>$ rightMouse $>$ $>$ $>$ $>$ $>$
2.409 -\item
2.410 - \begin{enumerate}
2.411 - \item
2.412 - \begin{enumerate}
2.413 - \item
2.414 - \begin{itemize}
2.415 - \item
2.416 - \begin{itemize}
2.417 - \item
2.418 - \item
2.419 - \item
2.420 - \end{itemize}
2.421 - \item
2.422 - \item
2.423 - \end{itemize}
2.424 - \item
2.425 - \item
2.426 - \end{enumerate}
2.427 - \item
2.428 - \item
2.429 - \end{enumerate}
2.430 -\item
2.431 - \begin{enumerate}
2.432 - \item
2.433 - \begin{enumerate}
2.434 - \item
2.435 - \begin{itemize}
2.436 - \item
2.437 - \begin{itemize}
2.438 - \item
2.439 - \item
2.440 - \item
2.441 - \end{itemize}
2.442 - \item
2.443 - \item
2.444 - \end{itemize}
2.445 - \item
2.446 - \item
2.447 - \end{enumerate}
2.448 - \item
2.449 - \item
2.450 - \end{enumerate}
2.451 +%$<$ $>$
2.452 +%Men\"u $>$ $>$ $>$ $>$ $>$ $>$
2.453 +%``Project''-View $>$ rightMouse $>$ $>$ $>$ $>$ $>$
2.454 +%\item
2.455 +% \begin{enumerate}
2.456 +% \item
2.457 +% \begin{enumerate}
2.458 +% \item
2.459 +% \begin{itemize}
2.460 +% \item
2.461 +% \begin{itemize}
2.462 +% \item
2.463 +% \item
2.464 +% \item
2.465 +% \end{itemize}
2.466 +% \item
2.467 +% \item
2.468 +% \end{itemize}
2.469 +% \item
2.470 +% \item
2.471 +% \end{enumerate}
2.472 +%\item
2.473 +%\item
2.474 +%\end{enumerate}
2.475 +%\item
2.476 +%\begin{enumerate}
2.477 +%\item
2.478 +%\begin{enumerate}
2.479 +%\item
2.480 +%\begin{itemize}
2.481 +%\item
2.482 +%\begin{itemize}
2.483 +%\item
2.484 +%\item
2.485 +%\item
2.486 +%\end{itemize}
2.487 +%\item
2.488 +%\item
2.489 +%\end{itemize}
2.490 +%\item
2.491 +%\item
2.492 +%\end{enumerate}
2.493 +%\item
2.494 +%\item
2.495 +%\end{enumerate}
2.496 \end{enumerate}
2.497
2.498
2.499 \section{Implementation der jEdit Komponenten}
2.500
2.501 \subsection{Erstellen des Plugin-Ger\"{u}sts}
2.502 -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.
2.503 +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.
2.504
2.505 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.
2.506
2.507 @@ -316,16 +351,20 @@
2.508 \end{enumerate}
2.509
2.510 \subsection{Verbindung zum Isabelle-Pure Plugin herstellen}
2.511 -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.
2.512 +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, {\tt Pure.jar}, weitergegeben werden. Dort k\"{o}nnen die Daten verwertet und aufbereitet zur\"{u}ck an das Frontend gereicht werden.
2.513
2.514 \begin{figure}
2.515 \begin{center}
2.516 -\includegraphics[width=100mm]{../fig-jedit-plugins-SD}
2.517 +\includegraphics[width=100mm]{../fig-jedit-plugins-SD.png}
2.518 \end{center}
2.519 \label{fig-jedit-plugins-SD}
2.520 +\caption{jEdit Plugins und die Verbindung zu Isabelle}
2.521 \end{figure}
2.522
2.523 -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.
2.524 +%Fig.\ref{fig-jedit-plugins-SD} WARUM GEHT DAS NICHT ???
2.525 +Fig.4.1 zeigt die involvierten Komponenten und ihren Zusammenhang.
2.526 +
2.527 +Der Zusammenhang zwischen dem Kern von Isabelle, Isabelle-Pure und dem Plugin wird folgenderma\ss en hergestellt: Zun\"{a}chst wird {\tt Pure.jar} leicht modifiziert, danach neu erstellt und zuletzt zu den restlichen jEdit-Plugins hinzugef\"{u}gt. 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.
2.528
2.529
2.530 \begin{enumerate}
2.531 @@ -338,45 +377,81 @@
2.532 Alle die oben angef\"{u}hrten Punkte, sowie das Erzeugen und Kopieren des Plugins selbst, werden vom Script isac\_jedit erledigt.
2.533 Das Skript kann dem Anhang C entnommen werden.
2.534
2.535 +\section{``Run Configurations''}
2.536 +Zwischen Isabelle2009-2 und Isabelle2011 hat sich viel ge\"andert. Jetzt mit Isabelle2011 sieht es folgenderma\ss en aus:
2.537 +
2.538 +Am Anfang der Plugin-Entwicklung wird man versuchen, ohne eine Verbindung zu Isabelle auszukommen; in sp\"ateren Phase wird man genau diese Verbindung brauchen. Starten eines Plugins in NB mit gleichzeitigem Hochfahren von Isabelle ist schwierig.
2.539 +
2.540 +Folgende M\"oglichkeiten gibt es beim Debuggen:
2.541 +
2.542 +\begin{enumerate}
2.543 +\item Man macht alles in Netbeans. Mit dem -Disabelle.home=... sollte man
2.544 + die Applikation direkt aus der IDE starten und profilen/debuggen
2.545 + k\"onnen. Das war der urspr\"ungliche Plan des ganzen Setups, d.h. der
2.546 + Grund warum er so kompliziert ist.
2.547 +
2.548 +\item Man startet aus der Shell \"uber "isabelle jedit -d" und verbindet
2.549 + dann den Netbeans debugger (oder jeden anderen JVM debugger) \"uber
2.550 + den hier ausgegebenen Port.
2.551 +
2.552 +\item Man startet "isabelle jedit", geht dann in das "Console" Plugin und
2.553 + w\"ahlt dort das "Scala" Sub-Plugin aus. Nach ca. 5s Bedenkzeit steht
2.554 + der interaktive Scala toplevel innerhalb von Isabelle/jEdit zur
2.555 + Verf\"ugung. Nun kann man direkt Dinge auswerten etc. und schauen was
2.556 + passiert.
2.557 +
2.558 + Auf dem Cambridge Workshop 2010, {\tt T06\_System.thy} sind Beispiele zu finden.
2.559 + Siehe subsection Isabelle/Scala. Man aktuviert dazu Isabelle/jEdit
2.560 + mit obigem thy File und kopiert die Scala snippets aus dem Text
2.561 + zeilenweise in das Console/Scala Fenster.
2.562 +
2.563 +\item Man streut einfach {\tt System.err.println} in seinen Code ein.
2.564 +\end{enumerate}
2.565 +Die M\"oglichkeiten (3) oder (4) sind zu bevorzugen.
2.566 +
2.567 +Ferner gibt es einige externe JVM Diagnose-Tools. Zu nennen sind {\tt jvisualvm} oder {\tt jconsole} um threads, heaps, profiles etc. anzuschauen, da sich das alles gerne verheddert.
2.568 +
2.569 +Richtig koordiniertes Hochfahren aller Komponenten braucht ein Shellscript wie {\tt isabelle jedit}.
2.570 +
2.571 \section{Umsetzung des SD-Parsers}
2.572 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.
2.573
2.574 -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.
2.575 +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.
2.576
2.577
2.578 \chapter{Ausblick: Von SD- zum \isac-Plugin}
2.579 -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.
2.580 +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.
2.581
2.582 -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.
2.583 +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.
2.584
2.585 \chapter{Zusammenfassung und R\"{u}ckblick}
2.586 Zusammenfassend wird nun ein \"Uberblick gegeben, welche Milestones erledigt wurden und welche nicht; Details dazu finden sich in Anhang A. %TODO
2.587 Abschlie{\ss}end gebe ich einen R\"uckblick auf meine pers\"onlichen Erfahrungen aus dieser Bakkalaureats-Arbeit.
2.588
2.589 -\section{Zusammenfassung}
2.590 +\section{Zusammenfassung}\label{zusammenfassung}
2.591 Folgende Milestones wurden erfolgreich abgeschlossen:
2.592 \begin{enumerate}
2.593 \item Relevante Isabelle Komponenten dokumentiert
2.594
2.595 \item Installation der Standard-Komponenten:
2.596 - \begin{itemize}
2.597 - \item Mercurial Versioncontrol
2.598 - \item NetBeans IDE
2.599 - \item Standard Isabelle Bundle
2.600 - \end{itemize}
2.601 -
2.602 +\begin{itemize}
2.603 +\item Mercurial Versioncontrol
2.604 +\item NetBeans IDE
2.605 +\item Standard Isabelle Bundle
2.606 +\end{itemize}
2.607 +
2.608 \item Entwicklungsumgebung vom Isabelle-Team kopieren
2.609 - \begin{itemize}
2.610 - \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
2.611 - \item jEdit als NetBeans Projekt definiert
2.612 - \end{itemize}
2.613 -
2.614 +\begin{itemize}
2.615 +\item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
2.616 +\item jEdit als NetBeans Projekt definiert
2.617 +\end{itemize}
2.618 +
2.619 \item Relevante Komponenten implementieren
2.620 - \begin{itemize}
2.621 - \item jEdit Plugin f\"ur SD
2.622 - \item Verbindung des Plugins zu Isabelle
2.623 - \item zugeh\"origen Parser: nur ein Test in SML
2.624 - \end{itemize}
2.625 +\begin{itemize}
2.626 +\item jEdit Plugin f\"ur SD
2.627 +\item Verbindung des Plugins zu Isabelle
2.628 +\item zugeh\"origen Parser: nur ein Test in SML
2.629 +\end{itemize}
2.630 \end{enumerate}
2.631
2.632 \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.
2.633 @@ -395,16 +470,16 @@
2.634
2.635 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.
2.636
2.637 -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.
2.638 +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.
2.639
2.640 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.
2.641
2.642 %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!
2.643
2.644 %\chapter{Milestones und Arbeitsprotokolle}
2.645 -%\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010}
2.646 +%\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010}
2.647 %\begin{itemize}
2.648 -%\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010
2.649 +%\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010
2.650 %\item Charakteristika der Programmsprache Scala: beendet am 27.09.2010
2.651 %\item Scala Actors: beendet am 12.08.2010
2.652 %\end{itemize}
2.653 @@ -414,11 +489,11 @@
2.654 %12.07.2010 & Meeting: erste Besprechung und Erkl\"{a}rungen zu Isabelle, Isac und CTPs & 2 \\ \hline
2.655 %15.07.2010 & Recherche \"{u}ber Isabelle und CTPs & 3 \\ \hline
2.656 %20.07.2010 & Meeting: Besprechen der grunds\"{a}tzlichen Vorgangsweise und Ziele & 1 \\ \hline
2.657 -%23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline
2.658 +%23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline
2.659 %30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise \"{u}ber Backs 'structured derivations'; Begriffserkl\"{a}rung & 3 \\ \hline
2.660 %01.08.2010 & Recherche: Buch f\"{u}r Scala & 2 \\ \hline
2.661 %03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
2.662 -%05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
2.663 +%05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
2.664 %06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
2.665 %08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
2.666 %09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
2.667 @@ -435,7 +510,7 @@
2.668 %\begin{itemize}
2.669 %\item Isabelle installiert, Filestruktur bekannt: beendet am 02.08.2010
2.670 %\item Scala in NetBeans eingebunden: beendet am 22.07.2010
2.671 -%\item Mercurial installiert und einrichten des Repositories: beendet am 19.07.2010
2.672 +%\item Mercurial installiert und einrichten des Repositories: beendet am 19.07.2010
2.673 %\end{itemize}
2.674 %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
2.675 %\hline
2.676 @@ -444,7 +519,7 @@
2.677 %20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
2.678 %21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
2.679 %22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
2.680 -%23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline
2.681 +%23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline
2.682 %27.07.2010 & Isabelle-jEdit-Plugin: \"{a}nderungen an der Projektstruktur & 7 \\ \hline
2.683 %28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
2.684 %29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
2.685 @@ -454,11 +529,11 @@
2.686 %\hline
2.687 %\end{tabular}
2.688 %
2.689 -%\section{NetBeans-Projekt aufgesetzt: beendet am 02.08.2010}
2.690 +%\section{NetBeans-Projekt aufgesetzt: beendet am 02.08.2010}
2.691 %\begin{itemize}
2.692 %\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: beendet am 02.08.2010
2.693 %\item jEdit-Plugin: XML-Files f\"{u}r ISAC vorbereitet: beendet am 22.07.2010
2.694 -%\item jEdit-Plugin: Source files geschrieben: beendet am 19.07.2010
2.695 +%\item jEdit-Plugin: Source files geschrieben: beendet am 19.07.2010
2.696 %\end{itemize}
2.697 %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
2.698 %\hline
2.699 @@ -467,17 +542,17 @@
2.700 %11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
2.701 %21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
2.702 %22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten f\"{u}r ISAC & 3 \\ \hline
2.703 -%24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline
2.704 +%24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline
2.705 %26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach L\"{o}sungen & 3 \\ \hline
2.706 %28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
2.707 %29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
2.708 %30.08.2010 & Isabelle-jEdit-Plugin endlich vollst\"{a}ndig lauff\"{a}hig gebracht & 4 \\ \hline
2.709 %01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
2.710 -%04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline
2.711 -%20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline
2.712 +%04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline
2.713 +%20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline
2.714 %22.09.2010 & Meeting: Fortschrittsbericht, kurze Einf\"{u}hrung f\"{u}r Mitstreiter & 3 \\ \hline
2.715 %
2.716 -%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
2.717 +%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
2.718 %30.09.2010 & QN: Start mit \"{u}bersetzten der Sourcefiles & 5 \\ \hline
2.719 %02.10.2010 & QN: \"{U}bersetzten der Sourcefiles & 6 \\ \hline
2.720 %04.10.2010 & QN: \"{U}bersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
2.721 @@ -486,7 +561,7 @@
2.722 %\hline
2.723 %\end{tabular}
2.724 %
2.725 -%\section{Experimentelle Parser implementiert: beendet am 04.03.2011}
2.726 +%\section{Experimentelle Parser implementiert: beendet am 04.03.2011}
2.727 %\begin{itemize}
2.728 %\item Experimente mit dem SideKick-Parser abgeschlossen: beendet am 03.02.2011
2.729 %\item Verbindung zu Isabelle-Pure hergestellt: beendet am 04.03.2011
2.730 @@ -501,7 +576,7 @@
2.731 %16.02.2011 & Erstellen des Isabelle-Pur jar-Files & 1 \\ \hline
2.732 %19.02.2011 & Behebung des Problems mit den Umgebungsvariablen & 1 \\ \hline
2.733 %03.03.2011 & Erzeugung des Pure.jar Package m\"{o}glich & 2 \\ \hline
2.734 -%04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet & 3 \\ \hline
2.735 +%04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet & 3 \\ \hline
2.736 %08.04.2011 & Besprechung: Implementierung des experimentellen Parsers wird nicht mehr durchgef\"{u}hrt & 1 \\ \hline \hline
2.737 % & Anzahl der Einheiten & 12 \\
2.738 %\hline
2.739 @@ -511,7 +586,7 @@
2.740 %\begin{itemize}
2.741 %\item Bacc.-Protokoll fertiggestellt: beendet am 01.03.2011
2.742 %\item Dokumentation: erste Version fertiggestellt: beendet am 28.04.2011
2.743 -%\item Dokumentation abgeschlossen: beendet am TO.DO.2011
2.744 +%\item Dokumentation abgeschlossen: beendet am TO.DO.2011
2.745 %\end{itemize}
2.746 %\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
2.747 %\hline
3.1 --- a/doc-src/isac/msteger/bakk-arbeit/master_thesis.bib Tue Jun 28 17:09:05 2011 +0200
3.2 +++ b/doc-src/isac/msteger/bakk-arbeit/master_thesis.bib Fri Jul 01 10:45:12 2011 +0200
3.3 @@ -1,4 +1,29 @@
3.4 % Add your bibtex entries
3.5 +
3.6 +@Book{aichernig:uni-iist-02,
3.7 + editor = {Aichernig, Bernhard K. and Maibaum, Tom},
3.8 + title = {Formal Methods at the Crossroads. From Panacea to Foundational Support.
3.9 +{10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University}},
3.10 + publisher = {Springer-Verlag},
3.11 + year = {2003},
3.12 + volume = {2757},
3.13 + series = {Lecture Notes in Computer Science},
3.14 + address = {Lisbon, Portugal},
3.15 + month = {March 18–20, 2002}
3.16 +}
3.17 +
3.18 +@InCollection{aichernig:mut-test,
3.19 + author = {Aichernig, Bernhard},
3.20 + title = {A systematic introduction to mutation testing in unifying theories of programming},
3.21 + booktitle = {Testing Techniques in Software Engineering},
3.22 + pages = {243-287},
3.23 + publisher = {Springer Berlin / Heidelberg},
3.24 + year = {2010},
3.25 + editor = {Borba, Paulo and Cavalcanti, Ana and Sampaio, Augusto and Woodcook, Jim},
3.26 + volume = {6153},
3.27 + series = {Lecture Notes in Computer Science}
3.28 +}
3.29 +
3.30 @inproceedings{Aspinall:2007:FIP:1420412.1420429,
3.31 author = {Aspinall, David and L\"{u}th, Christoph and Winterstein, Daniel},
3.32 title = {A Framework for Interactive Proof},
4.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis-acknowl.tex Tue Jun 28 17:09:05 2011 +0200
4.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-acknowl.tex Fri Jul 01 10:45:12 2011 +0200
4.3 @@ -11,10 +11,14 @@
4.4 %\vspace*{3mm}
4.5
4.6 \begin{changemargin}{1.5cm}{1.5cm}
4.7 -I would like to thank ...
4.8 +I would like to thank Professor Berhard Aichernig for having prepared the grounds for this thesis by his work on test case generation and in particular in his interest in the computer theorem prover Isabelle.
4.9 +
4.10 +His general surveys on computer theorem proving, on programming languages in general, on functional programming in particular and on respective advantages in upcoming multi-core computing were inspiring and they motivate the directions for my future studies.
4.11 +
4.12 +Many thanks also to Walther Neuper, who was always available for the many intricacies of Isabelle/Isar and the technicalities involved when doing a bachelor project and writing a thesis.
4.13
4.14 \begin{flushright}
4.15 -your name \\ {\small place, county, date}
4.16 +Marco Steger \\ {\small Graz, June 30, 2011}
4.17 \end{flushright}
4.18 \end{changemargin}
4.19
4.20 @@ -28,10 +32,16 @@
4.21 %\vspace*{0mm}
4.22
4.23 \begin{changemargin}{1.5cm}{1.5cm}
4.24 -Ich möchte mich herzlich bei allen bedanken, die ...
4.25 +Ich möchte mich herzlich bei allen bedanken, die diese Bakkalaureats-Arbeit unterst\"utzt haben.
4.26 +
4.27 +Herr Professor Bernhard Aichernig hat die Voraussetzungen f\"ur die Themenstellung der Arbeit durch seine F\&E in Test-Case-Generation geschaffen; Isabelle geh\"ort auch zu seinem Tool-Set.
4.28 +
4.29 +Besonder inspirierend waren seine \"Uberblicks-Informationen zu Computer Theorem Proving, zu Programm-Sprachen im Allgemeinen und zu funktionalen Sprachen im Besonderen, die ihre Vorteile bei den kommenden Multi-Core-Prozessoren zum Tragen bringen werden; diese Informationen werden auch meine Entscheidung f\"ur Wahlf\"acher in den kommenden Semestern motivieren.
4.30 +
4.31 +Walther Neuper war immer hilfreich in allen technischen Fragen zu Isabelle/Isar und in organisatorischen Fragen zu Bachelor-Projekt und -Thesis.
4.32
4.33 \begin{flushright}
4.34 -Dein Name \\ {\small Ort, Land, Datum}
4.35 +Marco Steger \\ {\small Graz, am 30 Juni 2011}
4.36 \end{flushright}
4.37 \end{changemargin}
4.38
5.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis-appendix.tex Tue Jun 28 17:09:05 2011 +0200
5.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-appendix.tex Fri Jul 01 10:45:12 2011 +0200
5.3 @@ -104,11 +104,11 @@
5.4 \hline
5.5 \end{tabular}
5.6
5.7 -\section{Verfassen der Dokumentation und abschliesende Arbeiten: beendet am TO.DO.2011}
5.8 +\section{Verfassen der Dokumentation und abschliesende Arbeiten: beendet am 30.Juni 2011}
5.9 \begin{itemize}
5.10 \item Bacc.-Protokoll fertiggestellt: beendet am 01.03.2011
5.11 \item Dokumentation: erste Version fertiggestellt: beendet am 28.04.2011
5.12 -\item Dokumentation abgeschlossen: beendet am TO.DO.2011
5.13 +\item Dokumentation abgeschlossen: beendet am 30.Juni 2011
5.14 \end{itemize}
5.15 \begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
5.16 \hline
5.17 @@ -298,42 +298,42 @@
5.18 echo "Done!" \\
5.19 }
5.20
5.21 -\chapter{Filestruktur f\"ur die Entwicklung des SD-Plugins}
5.22 +\chapter{Filestruktur f\"ur die Entwicklung des SD-Plugins}\label{files-SD-plugin}
5.23
5.24 -build.xml\\
5.25 -makedist\\
5.26 -manifest.mf\\
5.27 -README\_BUILD\\
5.28 -\textbf{build/*}\\
5.29 -\textbf{contrib/*}\\
5.30 -\textbf{dist/*}\\
5.31 -\textbf{plugin/}build.xml\\
5.32 -\textbf{plugin/}changes40.txt\\
5.33 -\textbf{plugin/}changes42.txt\\
5.34 -\textbf{plugin/}description.html\\
5.35 -\textbf{plugin/}IsacActions.java\\
5.36 -\textbf{plugin/}Isac.iml\\
5.37 -\textbf{plugin/}Isac.java\\
5.38 -\textbf{plugin/}IsacOptionPane.java\\
5.39 -\textbf{plugin/}IsacPlugin.java\\
5.40 -\textbf{plugin/}IsacTextArea.java\\
5.41 -\textbf{plugin/}IsacToolPanel.java\\
5.42 -\textbf{plugin/}plugin\\
5.43 -\textbf{plugin/}README.txt\\
5.44 -\textbf{nbproject/*}\\
5.45 -\textbf{src/}actions.xml\\
5.46 -\textbf{src/}changes40.txt\\
5.47 -\textbf{src/}changes42.txt\\
5.48 -\textbf{src/}description.html\\
5.49 -\textbf{src/}dockables.xml\\
5.50 -\textit{\textbf{src/}IsacActions.scala\\}
5.51 -\textbf{src/}Isac.iml\\
5.52 -\textit{\textbf{src/}IsacOptionPane.scala\\}
5.53 -\textit{\textbf{src/}IsacPlugin.scala\\}
5.54 -\textbf{src/}Isac.props\\
5.55 -\textit{\textbf{src/}Isac.scala\\}
5.56 -\textit{\textbf{src/}IsacTextArea.scala\\}
5.57 -\textit{\textbf{src/}IsacToolPanel.scala\\}
5.58 -\textbf{src/}manifest.mf\\
5.59 -\textbf{src/}README.txt\\
5.60 -\textbf{src/}users-guide.xml \\
5.61 \ No newline at end of file
5.62 +\textbf{src/Tools/jEditC/}build.xml\\
5.63 +\textbf{src/Tools/jEditC/}makedist\\
5.64 +\textbf{src/Tools/jEditC/}manifest.mf\\
5.65 +\textbf{src/Tools/jEditC/}README\_BUILD\\
5.66 +\textbf{src/Tools/jEditC/build/*}\\
5.67 +\textbf{src/Tools/jEditC/contrib/*}\\
5.68 +\textbf{src/Tools/jEditC/dist/*}\\
5.69 +\textbf{src/Tools/jEditC/plugin/}build.xml\\
5.70 +\textbf{src/Tools/jEditC/plugin/}changes40.txt\\
5.71 +\textbf{src/Tools/jEditC/plugin/}changes42.txt\\
5.72 +\textbf{src/Tools/jEditC/plugin/}description.html\\
5.73 +\textbf{src/Tools/jEditC/plugin/}testSDActions.java\\
5.74 +\textbf{src/Tools/jEditC/plugin/}testSD.iml\\
5.75 +\textbf{src/Tools/jEditC/plugin/}testSD.java\\
5.76 +\textbf{src/Tools/jEditC/plugin/}testSDOptionPane.java\\
5.77 +\textbf{src/Tools/jEditC/plugin/}testSDPlugin.java\\
5.78 +\textbf{src/Tools/jEditC/plugin/}testSDTextArea.java\\
5.79 +\textbf{src/Tools/jEditC/plugin/}testSDToolPanel.java\\
5.80 +\textbf{src/Tools/jEditC/plugin/}plugin\\
5.81 +\textbf{src/Tools/jEditC/plugin/}README.txt\\
5.82 +\textbf{src/Tools/jEditC/nbproject/*}\\
5.83 +\textbf{src/Tools/jEditC/src/}actions.xml\\
5.84 +\textbf{src/Tools/jEditC/src/}changes40.txt\\
5.85 +\textbf{src/Tools/jEditC/src/}changes42.txt\\
5.86 +\textbf{src/Tools/jEditC/src/}description.html\\
5.87 +\textbf{src/Tools/jEditC/src/}dockables.xml\\
5.88 +\textbf{src/Tools/jEditC/src/}testSDActions.scala\\
5.89 +\textbf{src/Tools/jEditC/src/}testSD.iml\\
5.90 +\textbf{src/Tools/jEditC/src/}testSDOptionPane.scala\\
5.91 +\textbf{src/Tools/jEditC/src/}testSDPlugin.scala\\
5.92 +\textbf{src/Tools/jEditC/src/}testSD.props\\
5.93 +\textbf{src/Tools/jEditC/src/}testSD.scala\\
5.94 +\textbf{src/Tools/jEditC/src/}testSDTextArea.scala\\
5.95 +\textbf{src/Tools/jEditC/src/}testSDToolPanel.scala\\
5.96 +\textbf{src/Tools/jEditC/src/}manifest.mf\\
5.97 +\textbf{src/Tools/jEditC/src/}README.txt\\
5.98 +\textbf{src/Tools/jEditC/src/}users-guide.xml \\
5.99 \ No newline at end of file
6.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis-biblio.tex Tue Jun 28 17:09:05 2011 +0200
6.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-biblio.tex Fri Jul 01 10:45:12 2011 +0200
6.3 @@ -1,6 +1,7 @@
6.4 {
6.5
6.6 -\bibliographystyle{plain}
6.7 +%\bibliographystyle{plain}
6.8 +\bibliographystyle{alpha}
6.9
6.10
6.11 % the names of the bib files used
6.12 @@ -8,7 +9,6 @@
6.13 \phantomsection
6.14 \addcontentsline{toc}{chapter}{Bibliography}
6.15 \bibliography{master_thesis.bib}
6.16 -%\bibliography{../master_thesis.bib}
6.17
6.18 }
6.19
7.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis-contents.tex Tue Jun 28 17:09:05 2011 +0200
7.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-contents.tex Fri Jul 01 10:45:12 2011 +0200
7.3 @@ -12,13 +12,14 @@
7.4 \titlespacing*{\section}{0em}{-2em}{1.5em}
7.5 \def\chapter*#1{\section*{#1}}
7.6
7.7 -\vspace*{20mm}
7.8 -\listoftables
7.9 -%\addcontentsline{toc}{chapter}{List of Tables}
7.10 +%\vspace*{20mm}
7.11 +%\listoftables
7.12 +%%\addcontentsline{toc}{chapter}{List of Tables}
7.13 +%
7.14 +%\vspace*{20mm}
7.15 +%\lstlistoflistings
7.16 +%%\addcontentsline{toc}{chapter}{List of Listings}
7.17
7.18 -\vspace*{20mm}
7.19 -\lstlistoflistings
7.20 -%\addcontentsline{toc}{chapter}{List of Listings}
7.21 }
7.22 }
7.23
8.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis-intro.tex Tue Jun 28 17:09:05 2011 +0200
8.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-intro.tex Fri Jul 01 10:45:12 2011 +0200
8.3 @@ -1,7 +1,9 @@
8.4 \chapter{Einf\"{u}hrung}
8.5 -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.
8.6 +Europa ist bei Computer Theorem Provern (CTP) weltweit f\"uhrend, die zwei prominenten Prover sind Coq \cite{coq1999} und Isabelle \cite{Paulson:Isa94}.
8.7 +Im Zuge der Weiterentwicklung der Informatik als Ingenieurs-Disziplin werden auch Anwendungsgebiete zunehmend mathematisiert \cite{db:dom-eng}, was wiederum CTP vermehrt auf den Plan ruft.
8.8 +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.
8.9
8.10 -Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software- Ingenieuren vorzudringen beginnen \cite{wolff10-boogie}, stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen.
8.11 -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.
8.12 +Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software- Ingenieuren vorzudringen beginnen (siehe zum Beispiel \cite{aichernig:uni-iist-02,aichernig:mut-test}),% \cite{wolff10-boogie},
8.13 +stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen. Einer der Vorschl\"age, wie Theorem Prover mit Front-ends zu verbinden w\"are, findet sich in \cite{Aspinall:2007:FIP:1420412.1420429}. Isabelle geht einen anderen Weg, indem es sich aktuellen technischen Herausforderungen stellt \cite{makarius:isa-scala-jedit}: 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.
8.14
8.15 -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.
8.16 +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) \cite{back-grundy-wright-98} sollen auf jEdit und Isabelle aufgesetzt werden. Die Bachelorarbeit liefert die Machbarkeits-Studie f\"ur diesen Schritt.
9.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis-title.tex Tue Jun 28 17:09:05 2011 +0200
9.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-title.tex Fri Jul 01 10:45:12 2011 +0200
9.3 @@ -6,8 +6,8 @@
9.4
9.5 \vspace{16mm}
9.6
9.7 -{\huge \bf Userinterfaces for Computer Theorem Prover\\
9.8 - feasibility study in the Isac-projekt\\}
9.9 +{\huge \bf Userinterfaces for Computer Theorem Provers\\
9.10 + Feasibility Study in the Isac-Projekt\\}
9.11
9.12 \vspace{16mm}
9.13
9.14 @@ -37,7 +37,7 @@
9.15 \end{tabular}}
9.16
9.17 \vfill
9.18 -{\large Graz, 30.05.2011????}
9.19 +{\large Graz, 30.06.2011}
9.20 \vspace{15mm}
9.21 \end{center}
9.22
9.23 @@ -118,12 +118,16 @@
9.24 \end{center}
9.25 \vspace*{7mm}
9.26
9.27 -Place english abstract here.
9.28 +The computer theorem prover Isabelle switches from a user interface for expert users to a user interface which is more powerful and which serves integration of Isabelle into other tools for software engineers.
9.29 +
9.30 +This bachelor thesis in ``Telematik'' introduces the specific components underlying Isabelle's new user interface, the scala-layer for asyncronous editing of proof documents, the Java-based editor jEdit together with the respective plugin mechanisms; and the thesis documents the current organization of these components in Isabelle and sets up the whole system, Isabelle, Scala and jEdit in the IDE NetBeans copying the configuration of the Isabelle developer team. This setup is explored in the implementation of a test-plugin, and the experiences are documented in detail.
9.31 +
9.32 +Thus the prerequisites are given for cooperation in the further development of Isabelle's future front-end and respective integration into development tools like test case generators for software engineers.
9.33
9.34 \vspace{5mm}
9.35 \noindent
9.36 {\large\bfseries Keywords:}
9.37 -some english keywords
9.38 +computer theorem prover, Isabelle, user-interface, jEdit, plugin, Scala, actors, asynconous communication, proof document, structured derivations
9.39
9.40
9.41
9.42 @@ -140,14 +144,14 @@
9.43
9.44 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.
9.45
9.46 -Die vorliegende Bachelorarbeit in Telematik f\"uhrt in die speziellen, dem 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. Es wird dazu ein SD-Test-Plugin umgesetzt. Ziel dieses Beispiel-Pugins ist in erster Linie eine Art HowTo f\"ur nachfolgende Projektarbeiten zu schaffen.
9.47 +Die vorliegende Bachelorarbeit in Telematik f\"uhrt in die speziellen, dem 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 setzt das gesamte System in einer integrierten Entwicklungsungebung auf. Dieses Setup wird in der Implementation eines Test-Plugins erprobt. Die Erfahrungen mit diesem Test werden ausf\"uhrlich dokumentiert.
9.48
9.49 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.
9.50
9.51 \vspace{5mm}
9.52 \noindent
9.53 {\large\bfseries Schlagworte:}
9.54 -einige deutsche Schlagworte
9.55 +Computer Theorem Proving, Isabelle, User-Interface, jEdit, Plugin, Scala, Actors, Asyncrone Kommunikation, Beweis-Dokument, Structured Derivations
9.56
9.57 \selectlanguage{english}
9.58 \end{changemargin}
10.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis.tex Tue Jun 28 17:09:05 2011 +0200
10.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis.tex Fri Jul 01 10:45:12 2011 +0200
10.3 @@ -64,6 +64,8 @@
10.4
10.5 %\backmatter
10.6 \include{thesis-biblio} % Bibliography
10.7 +%%%\bibliographystyle{plain}
10.8 +%%%\bibliography{master_thesis}
10.9 % \include{glossary} % Glossary
10.10 % \include{index} % Index
10.11
11.1 Binary file doc-src/isac/msteger/fig-jedit-plugins-SD.png has changed
12.1 Binary file doc-src/isac/msteger/fig-reuse-ml-scala-SD.odg has changed
13.1 Binary file doc-src/isac/msteger/fig-reuse-ml-scala-SD.png has changed
14.1 --- a/src/Tools/jEditC/nbproject/project.properties Tue Jun 28 17:09:05 2011 +0200
14.2 +++ b/src/Tools/jEditC/nbproject/project.properties Fri Jul 01 10:45:12 2011 +0200
14.3 @@ -27,7 +27,6 @@
14.4 file.reference.isabelle-jedit-src=src
14.5 file.reference.jedit.jar=../../../../../../home/makarius/lib/jedit/current/jedit.jar
14.6 file.reference.jedit.jar-1=../../../contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jedit.jar
14.7 -file.reference.Pure.jar=../../../../contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/Pure.jar
14.8 file.reference.src-Pure=../../Pure
14.9 includes=**
14.10 jar.compress=false
14.11 @@ -41,7 +40,6 @@
14.12 ${libs.SideKick.classpath}:\
14.13 ${libs.Console.classpath}:\
14.14 ${libs.Scala-compiler.classpath}:\
14.15 - ${file.reference.Pure.jar}:\
14.16 ${file.reference.jedit.jar-1}
14.17 # Space-separated list of extra javac options
14.18 javac.compilerargs=
