1.1 --- a/.hgignore Tue Jun 28 16:25:19 2011 +0200
1.2 +++ b/.hgignore Tue Jun 28 17:09:05 2011 +0200
1.3 @@ -16,6 +16,7 @@
1.4 ^doc-src/.*\.aux
1.5 ^doc-src/.*\.bbl
1.6 ^doc-src/.*\.blg
1.7 +^doc-src/.*\.brf
1.8 ^doc-src/.*\.dvi
1.9 ^doc-src/.*\.lot
1.10 ^doc-src/.*\.idx
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/bin/testSD Tue Jun 28 17:09:05 2011 +0200
2.3 @@ -0,0 +1,14 @@
2.4 +#!/usr/bin/env bash
2.5 +cd src/Pure/
2.6 +echo "Building Pure.jar"
2.7 +../../bin/isabelle env ./build-jars
2.8 +echo "copying Pure.jar to contrib/jedit"
2.9 +cp ../../lib/classes/Pure.jar ../../contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/
2.10 +echo "Building testSD.jar"
2.11 +cd /usr/local/isabisac/src/Tools/jEditC
2.12 +#ant jar
2.13 +#scala -jar "/usr/local/isabisac/src/Tools/jEditC/dist/jars/testSD.jar"
2.14 +cd /usr/local/isabisac/src/Pure/
2.15 +echo "copying testSD.jar to contrib/jedit"
2.16 +cp ../Tools/jEditC/contrib/jEdit/build/jars/testSD.jar ../../contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/
2.17 +echo "Done!"
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/isac/msteger/README Tue Jun 28 17:09:05 2011 +0200
3.3 @@ -0,0 +1,2 @@
3.4 +bakk-arbeit/ contains stylefiles required for Bernhard Aichernig's format.
3.5 +These probably go to a shared directory.
3.6 \ No newline at end of file
4.1 --- a/doc-src/isac/msteger/bakk-arbeit.tex Tue Jun 28 16:25:19 2011 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,280 +0,0 @@
4.4 -\documentclass{article}
4.5 -\usepackage{a4}
4.6 -\usepackage{times}
4.7 -\usepackage{latexsym}
4.8 -
4.9 -\bibliographystyle{alpha}
4.10 -\usepackage{graphicx}
4.11 -
4.12 -\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
4.13 -\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
4.14 -\def\Problem{ {\tt Problem }}
4.15 -
4.16 -\title{Userinterfaces f\"ur Computer Theorem Prover\\
4.17 - Machbarkeits-Studie im Isac-Projekt
4.18 -}
4.19 -
4.20 -\author{Marco Steger\\
4.21 -Bachelorarbeit Telematik\\
4.22 -am Institut f\"ur Softwaretechnologie\\
4.23 -TU Graz}
4.24 -
4.25 -\begin{document}
4.26 -\maketitle
4.27 -\abstract{
4.28 -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.
4.29 -
4.30 -Die vorliegende Bachelorarbeit in Telematik f\"uhrt in die speziellen, dem k\"unftigen Frontend zugrundleliegenden Konzepte und Komponenten (Scala-Layer f\"ur asynchrone Bearbeitung von Beweisdokumenten, jEdit mit Plugins, Parser) ein, dokumentiert die momentane Organisation dieser Komponenten im Isabelle System und implementiert das gesamte System in einer integrierten Entwicklungsungebung. Diese Implementation entspricht jener des Teils des Isabelle-Teams, das am neuen Frontend arbeitet.
4.31 -
4.32 -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.
4.33 -
4.34 -%Ziel des Projektes war es, die unz\"{a}hligen M\"{o}glichkeiten, die der Wechsel des Isabelle-Development-Teams vom veralteten Proof General in Verbinung mit dem Editor Emacs auf die neue Scala-Technoligie in Verbindung mit dem Java-Editor jEdit mit sich bringen und wie diese neuen Technologien hier an der TU Graz zum Ausbau des \sisac-Projektes genutzt werden k\"{o}nnen. Um die Weiterentwicklung voranzutreiben, wurden Schnittstellen identifiziert, an denen man an die bereits vorhandene Isabelle-jEdit-Implementierung andocken k\"{o}nnte und welche Vor- und Nachteile die f\"{u}r \sisac mit sich bringen. Weiters wurde der Editor jEdit und vorallem dessen Plugin-Managment-System durchleuchtet und ein Grund-Plugin f\"{u}r die Entwicklung des "structured derivations"-Plugins gelegt. Zuletzt wurde eine Schnittstelle zum Isabelle-Pure-Library implementiert.}
4.35 -
4.36 -\section{Einf\"{u}hrung}\label{intro}
4.37 -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.
4.38 -
4.39 -Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software-Ingenieuren vorzudringen beginnen, stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen.
4.40 -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.
4.41 -
4.42 -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.
4.43 -
4.44 -\section{Beleuchtung der Projektrelevanten Technologien}
4.45 -
4.46 -\subsection{Der Texteditor jEdit}\label{jEdit}
4.47 -% http://www.jedit.org/
4.48 -% http://de.wikipedia.org/wiki/JEdit
4.49 -% http://www.chip.de/downloads/jEdit_19235021.html
4.50 -%
4.51 -jEdit ist ein in Java geschriebener und als Open-Source-Projekt erh\"altlicher Texteditor, der vorallem durch sein sehr gut entwickeltes und ebenso einfaches Plugin-Managment-System sehr effektiv eingetzt werden kann. Solche Plugins k\"{o}nnen direkt in jEdit installiert oder durch manuelles hinzuf\"{u}gen eines Plugin-Paketes genutzt werden. Dadurch ist dieser Editor sehr flexibel in der Anwendung und kann den eigenen Bed\"{u}rfnissen perfekt angepasst werden.
4.52 -Diese Umst\"ande sind wohl auch der Grund, warum sich die Entwickler von Isabelle f\"ur diesen Editor entschieden haben. Hierbei ist zu erw\"{a}hnen, dass hier eine etwas modifizierte bzw. an Isabelle angepasste Version verwendet wird. Es empfiehlt sich daher, immer die aktuelle Version des Isabelle-jEdit-Editors (zB. aus dem Bundle erh\"{a}ltlich auf der Isabelle-Homepage) zu verwenden, da hier diverse Voreinstellungen vorgenommen wurden. In weiterer Folge wird mit jEdit immer diese modifizierte Version des Editors in Verbindung gebracht, da die Verwendung der Grundversion aus oben gennanten Gr\"{u}nden nicht zu empfehlen bzw. sinnvoll ist.
4.53 -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.
4.54 -
4.55 -\subsubsection{Das Plugin-System}
4.56 -% http://jedit.org/users-guide/writing-plugins-part.html
4.57 -Wie im vorigen Abschnitt bereits erw\"ahnt, ist es sehr einfach und bequem m\"oglich, geeignete Plugins zu installieren bzw. zu verwenden. Es stehen bereits sehr viele verschiedenste Plugins auf der jEdit-Homepage zur Verf\"{u}gung. Diese werden ebenfalls als Open-Source-Projekte angeboten und es bietet sich daher an, bereits verf\"ugbare und funktionierende Plugins als Teil eines neuen Plugins zu verwenden und gegebenenfalls kleine Modifikationen oder Erweiterungen an den Plugins durchzuf\"{u}hren. Im Beispiel von Isabelle wurden unter anderen die Plugins \textit{Sidekick} und \textit{Konsole} verwendent. Dabei ist es m\"oglich, dass Java-Plugins mit Scala-Plugins kombiniert werden und diese k\"{o}nnen auch problemlos miteinander kommunizieren.
4.58 -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.
4.59 -Es ist auch m\"{o}glich, selbst implementierte Plugins direkt zu den bereits vorhandenen jEdit-Plugins hizuzuf\"{u}gen. Dazu muss das erzeugte "Plugin".jar Paket ledigich in den jars-Ordner verschoben werden. Dieser OrdnerBeim Start von jEdit wird das neue Plugin automatisch erkannt und hinzugef\"{u}gt. Man muss aber darauf achten, dass \"{a}nderungen nur nach einem Neustart von jEdit \"{u}bernommen werden.
4.60 -
4.61 -
4.62 -\subsubsection{Pluginstruktur}
4.63 -Ein solches jEdit-Plugin muss nat\"{u}rlich einen gewissen Design umsetzen, um von jEdit korrekt ausgef\"{u}hrt werden zu k\"{o}nnen. Grunds\"{a}tzlich besteht ein solches Plugin aus den eigentlichen Sourcefiles und einigen XML- und Property-Datein.
4.64 -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.
4.65 -
4.66 -\subsection{Isabelle}
4.67 -Isabelle ist einer der f\"{u}hrenden CTPs und an dessen Weiterentwicklung wird st\"{a}ndig gearbeitet. Der letzte gro{\ss}e Schritt betraf den Umstieg von reinem ML auf die Mischsprache Scala. Weiters wurde der in die Jahre gekommene Proof General und der damit in Verbindung stehende Editor Emacs durch den vielseitigen Editor jEdit ersetzt. Dadurch ergeben sich auch f\"{u}r das laufende \sisac-Projekt an der TU Graz neue M\"{o}glichkeiten. Wichtig im Zusammenhang mit dieser Beschreibung ist wichtig zu erw\"{a}hnen, dass hier in weiterer Folge nur noch f\"{u}r jEdit bzw. Scala relevante Teile von Isabelle behandelt und beschrieben werden. Weiters ist wichtig zu wissen, dass f\"{u}r die bereits bestehende Struktur rund um Isablle-jEdit zwei wichtige Isabelle-Pakete zum Einsatz kommen. Auf diese Pakete soll in den n\"{a}chsten Passagen eingegangen werden.
4.68 -
4.69 -\subsubsection{Isabelle-Pure}
4.70 -In diesem Plugin ist der eigentliche CTP-Teil von Isabelle verpackt. Wichtig zu wissen ist, dass es hierzu keine graphische Oberfl\"{a}chen oder direkten zugang von seiten des Editors gibt. Jedoch ist nur hier eine Schnittstelle zum eigentlichen Proofer m\"{o}glich und deshalb f\"{u}r das \sisac-Projekt von zentraler Bedeutung. Stanardm\"{a}{\ss}ig ist bereits ein Pure.jar-Paket f\"{u}r jEdit vorhanden. Um SD umsetzten zu k\"{o}nnen, muss hier einen Schnittstelle zu Isabelle-Pure implementiert werden. Nach diesem Schritt kann das Plugin Pure.jar neu gebaut werden.
4.71 -
4.72 -\subsubsection{Isabelle-jEdit}
4.73 -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.
4.74 -An diesem Plugin wird von seiten der Isabelle-Entwickler sehr stark weitergearbeitet. Darum sollten hier wohl nicht zu viele, am besten nat\"{u}rlich keine \"{a}nderungen, vorgenommen werden. Der Umstand, dass sich einzellnen Plugins ganz einfach in einem anderen mitverwenden lassen, macht es m\"{o}glich, dass das \sisac-Plugin sehr einfach, im Idealfall von Seiten der Isabelle-Entwickler, in das Isabelle-jEdit-Plugin integriert werden kann.
4.75 -
4.76 -\subsubsection{Paketstruktur von Isabelle}
4.77 -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.
4.78 -Nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. \sisac von Bedeutung sind und und wo diese zu finden sind.
4.79 -
4.80 -
4.81 -\begin{itemize}
4.82 -\item \textit{contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, ...} Der Ordner contrib ist in der Repository-Version nicht vorhanden! Dieser kann dem Isabelle-Bundle entnommen werden. Hier befinden sich alle ben\"{o}tigten Zusatztools f\"{u}r Isabelle und darunter eben auch jEdit. In dem oben angef\"{u}hrten Ordner liegen alle Plugins bzw. dorthin werden alle Plugins kopiert, die zusammen mit jEdit gestartet werden sollen. Das oben angef\"{u}hrte Script \"{u}bernimmt genau diesen Kopiervorgang f\"{u}r Isac.jar und Pure.jar.
4.83 -\item \textit{lib/classes:} \textbf{isabelle-scala.jar, pure.jar;} Standardm\"{a}{\ss}ig ist dieser Ordner nicht vorhanden. Erst durch erzeugen der angef\"{u}hrten jar's wird dieser Ordner und die Pakete erstellt.
4.84 -\item \textit{src/Tools/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...}
4.85 -\item \textit{src/Tools/isac/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...} Diese beiden obigen Verzeichnisse sind, wie man an den sehr \"{a}hnlichen Pfadstruktur erkennen kann, \"{a}quivalent wobei der zweite Pfad zum \sisac-Etwicklungsverzeichnis geh\"{o}rt. Hier sind die f\"{u}r das Isabelle-jEdit- bzw. \sisac-Plugin ben\"{o}tigten Plugins und Pakete plus das erzeugte Plugin zu finden.
4.86 -\item \textit{src/Tools/isac/jEdit/contrib/jEdit/build/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...} Diesen Aufbau ben\"{o}tig man nur, wenn man das jEdit-Isac-Projekt direkt in NetBeans debuggen m\"{o}chte. Man erkennt, dass in diesem Verzeichnis der vollst\"{a}ndige Quellcode von jEdit plus allen Plugins, die zusammen mit jEdit gestartet werden sollen, hier zu finden sind. Wie aber bereits erw\"{a}hnt, ist vom direkten Debuggen generell abzuraten.
4.87 -\end{itemize}
4.88 -
4.89 -
4.90 -\subsection{Die Programmiersprache Scala}
4.91 -Urspr\"{u}nglich wurde Isabelle rein in ML entwickelt. Erst vor ein paar Jahren wurde mit der \"{U}bersetzung von einigen Teilen in Scala begonnen. Grund genug, sich hier kurz diese neue und sehr vielseitige Sprache etwas anzusehen.
4.92 -
4.93 -\subsubsection{Grundlage der Sprache}
4.94 -Scala ist eine objektorientierte Sprache die sehr \"{a}hnlich zu Java aufgebaut wurde. Dadurch wird die Einarbeitung in diese Programmiersprache f\"{u}r Java-Programmierer sehr vereinfacht. Neben der Vorteilen einer objektorientierten Sprache deckt Scala aber auch die Bed\"{u}rfnisse der funktionalen Programmierung werden mit Scala abgedeckt. Dies ist wohl der Hauptgrund warum sich das Isabelle-Entwicklungsteam f\"{u}r diese Sprache entschieden hat. Wie breits erw\"{a}hnt ist Scala sehr \"{a}hnlich aufgebaut wie Java und hat nebenbei noch den gro{\ss}en Vorteil, das Scala-Executables in der JVM (Java virtual Machine) ausf\"{u}hrbar sind. Dadurch ist die Plattformunabh\"{a}ngigkeit garantiert und es besteht daher ein direkter Zusammenhang zwischen Scala und Java der auch bei der jEdit-Plugin-Entwiklung ausgenutzt bzw. verwedendet wird.
4.95 -
4.96 -Dieser direkte Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing gezeigt bzw. die Vorteile, die daraus resultieren beleuchtet werden.
4.97 -
4.98 -Beide Sprachen stellen diese Grafik-Bibliotheken zur Verf\"{u}gung (und darin auch eigene Shapes und Funktionalit\"{a}t). Es ist jedoch m\"{o}glich, Java-Bibliotheken, wie eben auch Java-Swing in Scala zu verwenden. Ein JButton(Java) kann zum Beispiel mittels \textit{import javax.swing.JButton} in Scala eingebunden und damit sofort auch verwendet werden. Auch Scala stellt in seiner Swing-Bibliothek eine Button zur Verf\"{u}gung: \textit{scala.swing.Button}. Es wird nahezu die selbe Funktionalit\"{a}t angeboten und teilweise die Erzeugung bzw. Verwendung vereinfacht. Man kann sich nun fragen, warum sich die Scala-Entwickler einerseit die M\"{u}he gemacht haben, die Verwendung Java-Swing, wie in Java selbst, m\"{o}glich zu machen und andererseits mit Scala-Swing eine nahezu idente Alternative geschaffen haben.
4.99 -
4.100 -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.
4.101 -Ein Letztes Problem bleibt noch: Es ist zwar sehr einfach ein Java-Swing-Objekt an einen Scala-Swing-Container (zb. Frame) anzubinden, da eine Konvertierung einer Java-Komponente in ein Scala-\"{a}quivalent problemlos m\"{o}glich ist. Jedoch ist oft auch die der Konvertierung einer Scala- in eine Java-Komponente n\"{o}tig. Dies kann ganz einfach mittels \textit(peer)-Befehl der Komponente erreicht werden.
4.102 -
4.103 -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.
4.104 -
4.105 -\subsubsection{Scala, Java und jEdit}
4.106 -Wie im letzten Abschnitt bereits beschrieben, kommen bei jEdit Java- sowie auch Scala-Komponenten zum Einsatz bzw. werden sogar zu logischen Einheiten kombiniert. So ist zum Beispiel jEdit selbst rein in Java geschrieben und das Plugin Isabelle-jEdit rein in Scala. Trotzdem gibt es \"{u}berhaupt kein Problem diese beiden jar-File miteinander bzw. innereinander in der JVM zu nutzen. Es geht sogar so weit, dass es m\"{o}glich ist, dass das Plugin Isabelle-jEdit bereits vorhandene und rein in Java geschriebene Plugins erweitert und nutzt. Dieses Zusammenspiel zwischen Objekten aus zwei verschiedenen Sprachen ist doch recht aussergew\"{o}hnlich und kann bzw sollte nat\"{u}rlich auch f\"{u}r SD bzw. \sisac ausgenutzt werden!
4.107 -
4.108 -
4.109 -\section{Aufbau des SD-Plugins}
4.110 -Dieses Kapitel soll nun anhand der bereits gewonnen Erkenntnise illustrieren, wie die wichtigsten Schritte zum SD-Plugin f\"{u}r jEdit wahrscheinlich aussehen werden.
4.111 -Wobei einige Schritte parallel und dadurch nat\"{u}rlich sehr gut im Team umgesetzt werden kann.
4.112 -
4.113 -\subsection{Erstellen des Plugin-Ger\"{u}sts}
4.114 -Hier gilt es, erstmal den Umfang der gew\"{u}nschten Anforderungen an das Plugin so genau wie m\"{o}glich zu identifizieren. Hat man eine sehr genaue Vorstellung, wie das GUI des Plugins aussehen wird und welche Zusatz-Features angeboten werden sollen so kann man gezielt untern den bereits bestehenden Plugins f\"{u}r jEdit nach n\"{u}tzlichen Plugins suchen, die in das SD-Plugin (m\"{o}glicherweise durch kleine Modifikationen) integriert werden k\"{o}nnen. Dies spart einerseits sehr viel Zeit und ist nebenbei genau die Art von Programmierung die durch die offnene Plugin-Struktur von jEdit gef\"{o}rdert wird.
4.115 -
4.116 -Hat man nun die Planung abgeschlossen und m\"{o}glicherweise n\"{u}tzliche Plugins gefunden, kann mit der Programmierung des GUIs begonnen werden. Man sollte hier beachten, dass man von Beginn an festlegt, ob mit Scala- oder Java-Swing Komponenten gearbeitet werden soll. Es ist zwar m\"{o}glich, beide Formen zu mischen, doch aus Klarheitsgr\"{u}nden sollte man sich doch f\"{u}r eine Art entscheiden. Wobei hier die Empfehlung im Moment eher noch Richtung Java-Swing geht, da man hier eigentlich f\"{u}r jede Art von Problem bzw. Aufgabe bereits HowTo's im Web finden kann. Da bei Scala-Swing nur Wrapper auf die Java-Swing-Libraries gesetzt wurden, entsteht dadurch auch keinerlei Performance-Verlust.
4.117 -
4.118 -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.
4.119 -
4.120 -\subsection{Erzeugung des Plugins}
4.121 -Hat man die Planung des Plugin-Ger\"{u}sts abgeschlossen und die eigentliche Implementationsphase begonnen, kann dieses Plugin getestet bzw. erzeugt und via jEdit ausgef\"{u}hrt werden. Dazu muss zuerst das jar-Filer erzeugt werden und danach in den jEdit-Pluginsordner verschoben werden. Die Erzeugung kann nat\"{u}rlich dirket mittels NetBeans durchgef\"{u}hrt werden. Doch es ist auch m\"{o}glich dies via Kommandline durchzuf\"{u}hren. Folgende Schritte illustrieren wie die Erzeugung und der Kopiervorgang des Plugins durchgef\"{u}hrt werden kann(Ausschnitt aus dem Skript isac\_jedit):
4.122 -\begin{enumerate}
4.123 -\item Das Plugin kann mittels Kommandline folgenderma{\ss}en erstellt werden: \textit{cd ISABELLE\_HOME/src/Tools/isac/jEdit} $\rightarrow$ \textit{ant jar}
4.124 -\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/}
4.125 -\item jEdit ausf\"{u}hren und testen
4.126 -\end{enumerate}
4.127 -
4.128 -\subsection{Verbindung zum Isabelle-Pure Plugin herstellen}
4.129 -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.
4.130 -
4.131 -Um diesen Schritt setzten zu k\"{o}nnen, muss eine Schnittstelle zwischen dem Kern von Isabelle, Isabelle-Pure und dem Plugin hergestellt werden. Dazu muss zun\"{a}chst Pure.jar leicht modifiziert, danach neu erstellt und zuletzt zu den restlichen jEdit-Plugins hizugef\"{u}gt werden. Dies wurde auf der aktuellen Version am Repository bereits erledigt. Folgende Schritte wurden dazu gesetzt und sind wieder n\"{o}tig, da sicher weitere Modifikationen an der Datei Pure.jar n\"{o}tig sein werden.
4.132 -
4.133 -\begin{enumerate}
4.134 -\item Um den \sisac-Teil im Isabelle-Pure genau abzugrenzen, wurde ein Ordner \textit{Isac} angelegt und ein Testfile \textit{isac.scala} erstellt.
4.135 -\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.
4.136 -\item Nun kann Pure.jar mittels Kommandline erstellt werden: \textit{cd /src/Pure} $\rightarrow$ \textit{../../bin/isabelle env ./build-jars}
4.137 -\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/}
4.138 -\item jEdit ausf\"{u}hren und testen
4.139 -\end{enumerate}
4.140 -Alle die oben angef\"{u}hrten Punkte sowie das Erzeugen und Kopieren des Plugins selbst wird vom Script isac\_jedit erledigt.
4.141 -
4.142 -\subsection{Umseztung des SD-Parsers}
4.143 -Aus Zeitgr\"{u}nden wurde dieser Punkt im Zuge dieser Projektarbeit nicht mehr umgesetzt. Jedoch gibt es bereits eine Version des Parsers in ML und kann in einigen Arbeitsstunden in Zusammenarbeit mit Herrn Neuper in Scala \"{u}bersetzt und eingesetzt werden.
4.144 -
4.145 -\section{Ausblick: Von SD- zum \isac-Plugin}
4.146 -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.
4.147 -
4.148 -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.
4.149 -
4.150 -\section{Milestones und Arbeitsprotokolle}
4.151 -\subsection{Inhaltliche Voraussetzungen erarbeitet: am 27.09.2010}
4.152 -\begin{itemize}
4.153 -\item Kenntnis der Grundlagen und Anwendung von CTP: am 03.08.2010
4.154 -\item Charakteristika der Programmsprache Scala: 27.09.2010
4.155 -\item Scala Actors: am 12.08.2010
4.156 -\end{itemize}
4.157 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.158 -\hline
4.159 -Datum & T\"atigkeit & Einheiten \\ \hline
4.160 -12.07.2010 & Meeting: erste Besprechung und Erkl\"{a}rungen zu Isabelle, Isac und CTPs & 2 \\ \hline
4.161 -15.07.2010 & Recherche \"{u}ber Isabelle und CTPs & 3 \\ \hline
4.162 -20.07.2010 & Meeting: Besprechen der grunds\"{a}tzlichen Vorgangsweise und Ziele & 1 \\ \hline
4.163 -23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline
4.164 -30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise \"{u}ber Backs 'structured derivations'; Begriffserkl\"{a}rung & 3 \\ \hline
4.165 -01.08.2010 & Recherche: Buch f\"{u}r Scala & 2 \\ \hline
4.166 -03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
4.167 -05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
4.168 -06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
4.169 -08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
4.170 -09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
4.171 -12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
4.172 -24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
4.173 -25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
4.174 -27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline \hline
4.175 - & Anzahl der Einheiten & 44 \\
4.176 -\hline
4.177 -\end{tabular}
4.178 -
4.179 -
4.180 -\subsection{Technische Voraussetzungen hergestellt: am 02.08.2010}
4.181 -\begin{itemize}
4.182 -\item Isabelle installiert, Filestruktur bekannt: am 02.08.2010
4.183 -\item Scala in NetBeans eingebunden: am 22.07.2010
4.184 -\item Mercurial installiert und einrichten des Repositories: 19.07.2010
4.185 -\end{itemize}
4.186 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.187 -\hline
4.188 -Datum & T\"atigkeit & Einheiten \\ \hline
4.189 -19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
4.190 -20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
4.191 -21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
4.192 -22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
4.193 -23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline
4.194 -27.07.2010 & Isabelle-jEdit-Plugin: \"{a}nderungen an der Projektstruktur & 7 \\ \hline
4.195 -28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
4.196 -29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
4.197 -30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung \"{u}ber Erfahrungen mit Filestruktur & 4 \\ \hline
4.198 -02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
4.199 - & Anzahl der Einheiten & 60 \\
4.200 -\hline
4.201 -\end{tabular}
4.202 -
4.203 -\subsection{NetBeans-Projekt aufgesetzt }% am ..(*)...}
4.204 -\begin{itemize}
4.205 -\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: am 02.08.2010
4.206 -\item jEdit-Plugin: XML-Files f\"{u}r ISAC vorbereitet: am 22.07.2010
4.207 -\item jEdit-Plugin: Source files geschrieben: 19.07.2010
4.208 -\end{itemize}
4.209 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.210 -\hline
4.211 -Datum & T\"atigkeit & Einheiten \\ \hline
4.212 -10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
4.213 -11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
4.214 -21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
4.215 -22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten f\"{u}r ISAC & 3 \\ \hline
4.216 -24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline
4.217 -26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach L\"{o}sungen & 3 \\ \hline
4.218 -28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
4.219 -29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
4.220 -30.08.2010 & Isabelle-jEdit-Plugin endlich vollst\"{a}ndig lauff\"{a}hig gebracht & 4 \\ \hline
4.221 -01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
4.222 -04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline
4.223 -20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline
4.224 -22.09.2010 & Meeting: Fortschrittsbericht, kurze Einf\"{u}hrung f\"{u}r Mitstreiter & 3 \\ \hline
4.225 -
4.226 -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
4.227 -30.09.2010 & QN: Start mit \"{u}bersetzten der Sourcefiles & 5 \\ \hline
4.228 -02.10.2010 & QN: \"{U}bersetzten der Sourcefiles & 6 \\ \hline
4.229 -04.10.2010 & QN: \"{U}bersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
4.230 -05.10.2010 & QN: QN vollständig in Scala \"{u}bersetzt, testen & 2 \\ \hline \hline
4.231 - & Anzahl der Einheiten & 71 \\
4.232 -\hline
4.233 -\end{tabular}
4.234 -
4.235 -\subsection{Experimentelle Parser implementiert}% am ..(*)...}
4.236 -\begin{itemize}
4.237 -\item Experimente mit dem SideKick-Parser abgschlossen: am 03.02.2011
4.238 -\item Verbindung zu Isabelle-Pure hergestellt: am 04.03.2011
4.239 -\item Implementierung des experimentellen Parsers: aus Zeitgr\"{u}nden nicht mehr durchgef\"{u}hrt
4.240 -\end{itemize}
4.241 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.242 -\hline
4.243 -Datum & T\"atigkeit & Einheiten \\ \hline
4.244 -28.01.2011 & Testen des SideKick-Parsers im Isabelle-Plugin & 2 \\ \hline
4.245 -29.01.2011 & Leichte Modifikationen des SideKick-Parsers im Isabelle-Plugin & 1 \\ \hline
4.246 -08.02.2011 & Besprechung zum Abschluss der praktischen Arbeiten & 1 \\ \hline
4.247 -16.02.2011 & Erstellen des Isabelle-Pur jar-Files & 1 \\ \hline
4.248 -19.02.2011 & Behebung des Problems mit den Umgebungsvariablen & 1 \\ \hline
4.249 -03.03.2011 & Erzeugung des Pure.jar Package m\"{o}glich & 2 \\ \hline
4.250 -04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet & 3 \\ \hline
4.251 -08.04.2011 & Besprechung: Implementierung des experimentellen Parsers wird nicht mehr durchgef\"{u}hrt & 1 \\ \hline \hline
4.252 - & Anzahl der Einheiten & 12 \\
4.253 -\hline
4.254 -\end{tabular}
4.255 -
4.256 -\subsection{Verfassen der Dokumentation und abschliesende Arbeiten: am 02.08.2010}
4.257 -\begin{itemize}
4.258 -\item Bacc.-Protokoll fertiggestellt: am 01.03.2011
4.259 -\item Dokumentation: erste Version fertiggestellt: am 28.04.2011
4.260 -\item Dokumentation abgeschlossen am: TO.DO.2011
4.261 -\end{itemize}
4.262 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.263 -\hline
4.264 -Datum & T\"atigkeit & Einheiten \\ \hline
4.265 -01.03.2011 & Besprechung zum Ablauf der Dokumentationsarbeiten: Protokoll und Dokumentation & 1 \\ \hline
4.266 -01.03.2011 & Erstellen des Protokolls & 2 \\ \hline
4.267 -08.03.2011 & Besprechung zur Doku und zur Schnittstelle zu Isabelle-Pure & 1 \\ \hline
4.268 -17.03.2011 & Dokumentation schreiben & 2 \\ \hline
4.269 -19.03.2011 & Dokumentation schreiben & 3 \\ \hline
4.270 -24.04.2011 & Dokumentation schreiben & 2 \\ \hline
4.271 -25.04.2011 & Dokumentation schreiben & 4 \\ \hline
4.272 -27.04.2011 & Dokumentation schreiben & 2 \\ \hline
4.273 -28.04.2011 & Dokumentation: Fertigstellen der ersten Version & 3 \\ \hline \hline
4.274 - & Anzahl der Einheiten & 20 \\
4.275 -\hline
4.276 -\end{tabular}
4.277 -
4.278 -\subsection{Pr\"asentation der Arbeit im IST-Seminar }% am ..(*)...}
4.279 -
4.280 -
4.281 -\bibliography{Doku}
4.282 -%\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}
4.283 -\end{document}
4.284 \ No newline at end of file
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/isac/msteger/bakk-arbeit/content.tex Tue Jun 28 17:09:05 2011 +0200
5.3 @@ -0,0 +1,532 @@
5.4 +\chapter{Definition der Aufgabenstellung}
5.5 +\section{Detaillierte Beschreibung der Aufgabenstellung}
5.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.
5.7 +
5.8 +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.
5.9 +
5.10 +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.
5.11 +Die nachfolgende Auflistung soll die wichtigsten Tasks nochmals zusammenfassen:
5.12 +\begin{enumerate}
5.13 +\item Relevante Isabelle Komponenten identifizieren und studieren
5.14 +\item Installation der Standard-Komponenten
5.15 +\item Entwicklungsumgebung vom Isabelle-Team kopieren
5.16 +\item Relevante Komponenten implementieren
5.17 + \begin{itemize}
5.18 + \item jEdit Plugin f\"ur SD
5.19 + \item zugeh\"origen Parser
5.20 + \item nicht vorgesehen: SD-Interpreter in Isar (SML)
5.21 + \end{itemize}
5.22 +\end{enumerate}
5.23 +
5.24 +\chapter{Beleuchtung der Projekt-relevanten Technologien}
5.25 +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.
5.26 +\section{Back's Structured Derivations}
5.27 +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.
5.28 +
5.29 +Das nachfolgende Beispiel zeigt ein einfaches Beispiel, wie eine Formel mittels SD dargestellt bzw. umgeformt werden kann:
5.30 +
5.31 +%{\footnotesize
5.32 +\begin{tabbing}
5.33 +123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
5.34 +\>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
5.35 +\> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
5.36 +\>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
5.37 +\> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
5.38 +\>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
5.39 +\> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
5.40 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
5.41 +\> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
5.42 +\> \>$\equiv$\>\vdots\\
5.43 +\> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
5.44 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
5.45 +\> \> \>$1 + -1 * x$\\
5.46 +\>\dots\>$1 + -1 * x$\\
5.47 +\>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
5.48 +\> \>$1-x$
5.49 +\end{tabbing}
5.50 +%}
5.51 +
5.52 +Dieses Beispiel kann wie folgt interpretiert werden:
5.53 +\begin{enumerate}
5.54 +\item Die erste Zeile ist als Angabe bzw. Ausgangspunkt der Berechnung zu verstehen.
5.55 +\item Nun folgt der eigentliche Ablauf einer Umformung mittels SD: Mit der Formel in der zweiten Zeile beginnt die Berechnung.
5.56 +\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.
5.57 +\item Aus dieser Rechenvorschrift ergibt sich die Formel in der n\"achsten Zeile.
5.58 +\item Dieser Ablauf wiederholt sich und zieht sich \"uber die weiteren Berechnungen.
5.59 +\end{enumerate}
5.60 +
5.61 +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.
5.62 +
5.63 +\section{Der Texteditor jEdit}\label{jEdit}
5.64 +% http://www.jedit.org/
5.65 +% http://de.wikipedia.org/wiki/JEdit
5.66 +% http://www.chip.de/downloads/jEdit_19235021.html
5.67 +%
5.68 +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.
5.69 +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.
5.70 +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.
5.71 +
5.72 +\subsection{Das Plugin-System}
5.73 +% http://jedit.org/users-guide/writing-plugins-part.html
5.74 +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.
5.75 +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.
5.76 +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.
5.77 +
5.78 +
5.79 +\subsection{Pluginstruktur}
5.80 +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.
5.81 +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.
5.82 +
5.83 +\section{Isabelle}
5.84 +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.
5.85 +
5.86 +\subsection{Isabelle-Pure}
5.87 +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.
5.88 +Eine Auflistung der f\"ur das Isabelle-Pure-Packet ben\"otigten Scala-Source-Filles kann Anhang B.2 entnommen werden.
5.89 +
5.90 +\subsection{Isabelle-jEdit}
5.91 +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.
5.92 +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.
5.93 +
5.94 +\subsection{Paketstruktur von Isabelle}
5.95 +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.
5.96 +Die nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. {\sisac} von Bedeutung sind und und wo diese zu finden sind.
5.97 +
5.98 +
5.99 +\begin{itemize}
5.100 +\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.
5.101 +\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.
5.102 +\item \textit{src/Tools/jEdit/dist/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, jedit.jar, ...}
5.103 +\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.
5.104 +\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.
5.105 +\end{itemize}
5.106 +
5.107 +Siehe dazu auch Anhang B. Dort sind alle relevanten jar-Pakete noch einmal aufgearbeitet und entsprechend gruppiert.
5.108 +
5.109 +\section{Die Programmiersprache Scala}
5.110 +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.
5.111 +
5.112 +\subsection{Grundlage der Sprache}
5.113 +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.
5.114 +
5.115 +Dieser direkte Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing gezeigt bzw. die Vorteile, die daraus resultieren, beleuchtet werden.
5.116 +
5.117 +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.
5.118 +
5.119 +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.
5.120 +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.
5.121 +
5.122 +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.
5.123 +
5.124 +\subsection{Scala, Java und jEdit}
5.125 +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!
5.126 +
5.127 +\subsection{Der Isabelle-Scala-Layer}
5.128 +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.
5.129 +
5.130 +Dieser Absatz sollen nun die Eigenschaften des Scala-Layers und die damit verbundenen Chancen f\"ur das Isac- bzw. SD-Projektes
5.131 +erarbeitet werden.
5.132 +
5.133 +\begin{figure}
5.134 +\begin{center}
5.135 +\includegraphics[width=100mm]{../fig-reuse-ml-scala-SD}
5.136 +\end{center}
5.137 +\label{fig-reuse-ml-scala}
5.138 +\end{figure}
5.139 +
5.140 +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.
5.141 +
5.142 +\chapter{Konfiguration und Implementation der Komponenten}
5.143 +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.
5.144 +
5.145 +\section{Konfiguration des Netbeans Projektes}
5.146 +Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das Netbeans-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert.
5.147 +
5.148 +\begin{enumerate}
5.149 +\item Konfigurations-Files von Netbeans in ``Files''-View; beeinflussen sich gegenseitig
5.150 + \begin{enumerate}
5.151 + \item build.xml (aus template erzeugt, keine automatischen Ver\"anderunen)
5.152 + \item nbproject/build-impl.xml (z.T. automatische Ver\"anderunen)
5.153 + \item nbproject/project.xml (z.T. automatische Ver\"anderunen)
5.154 + \item TODO
5.155 + \end{enumerate}
5.156 +\item Sacla-plugin installieren laut http://wiki.netbeans.org/Scala69,
5.157 + \begin{enumerate}
5.158 + \item von ``Install with NetBeasn 6.9''
5.159 + \item nach /usr/local/netbeans.../plugins/scala
5.160 + \end{enumerate}
5.161 +\item Scala-plugin installiert in NetBeans
5.162 + \begin{enumerate}
5.163 + \item Men\"u $>$ Tools $>$ Plugins $>$ Downloaded $>$ Add Plugins
5.164 + \item alle Files von /usr/local/netbeans.../plugins/scala/
5.165 + \item Fenster zeigt alle ausgew\"alten Files
5.166 + \item $<$Install$>$ calls Wizzard $<$Next$>$ probably accept Warning
5.167 + \item Funktionstest: Men\"ue $>$ Files $>$ New Project: zeigt Scala als ``Categories''
5.168 + \end{enumerate}
5.169 +\item Neues Projekt ``isac-jedit'' konfigurieren
5.170 + \begin{enumerate}
5.171 + \item Men\"u $>$ Open Project (weil schon aus dem Repository die notwendigen Files vorhanden sind)
5.172 + \item /src/Tools/jeditC: Reference Problems, weil jEdit folgende Plugins braucht
5.173 + \item Funktionskontrolle: ``Projects''-View zeigt das neue Projekt
5.174 + \item Die Konfigurations-Files sind v\"ollig getrennt von anderen Projekten
5.175 + \item Referenz-Probleme beheben; das zeigt auch eventuell fehlende Files
5.176 + \begin{enumerate}
5.177 + \item ``Projects''-View $>$ rightMouse $>$ Resolve Reference Problems: Fenster zeigt dieListe der fehlenden Dateien; $<$Next$>$
5.178 + \item Files holen aus ``Tools'' $>$ Libraries: \"uber Filebrowser aus dem Isabelle\_bundle holen contrib/jEdit---/jars
5.179 + \item ``New Library''
5.180 + \begin{enumerate}
5.181 + \item Cobra-renderer: cobra.jar
5.182 + \item Console: Console.jar
5.183 + \item ErrorList: ErrorList.jar
5.184 + \item Hyperlinks: Hyperlinks.jar
5.185 + \item Isabelle-Pure: Pure.jar
5.186 + \item Rhino-JavaScript: js.jar
5.187 + \item Scala-compiler: scala-compiler.jar
5.188 + \item SideKick: SideKick.jar
5.189 + \end{enumerate}
5.190 + \item Funktions-Kontrollen
5.191 + \begin{enumerate}
5.192 + \item das kleine gelbe Warndreieck im ``Projects''-View ist verschwunden
5.193 + \item im ``Projects''-View 2 Ordner: ``src'' und ``Libraries''
5.194 + \end{enumerate}
5.195 + \end{enumerate}
5.196 + \item jEdit-Paket zum ``isac-jedit''-Projekt hinzuf\"ugen
5.197 + \begin{enumerate}
5.198 + \item ``Project''-View $>$ rightMouse $>$ Add Jar/Folder: Filebrowser
5.199 + \item /contrib/jedit.../jedit.jar
5.200 + \item Funktions-Kontrolle: ist in ``Projects''/Libraries/jedit.jar
5.201 + \end{enumerate}
5.202 + \item Das neue Projekt ``isac-jedit'' zum Hauptprojekt machen: ``Project''-View $>$ rightMouse $>$ Set as Main Project; Funktions-Kontrolle: der Projektname ist boldface.
5.203 + \end{enumerate}
5.204 +\item Ab nun wird die Konfiguration \"uber ``trial and error'' zu Ende gef\"uhrt
5.205 + \begin{enumerate}
5.206 + \item Men\"u $>$ Build Main
5.207 + \begin{enumerate}
5.208 + \item Wenn: Target ``Isac-impl.jar'' does not exist in the project ``isac-jedit''. It is used from target ``debug''
5.209 + \begin{enumerate}
5.210 + \item Versuch
5.211 + \begin{itemize}
5.212 + \item build-impl.xml l\"oschen
5.213 + \item NetBeans neu starten, stellt build-impl.xml automatisch aus build.xml wieder her
5.214 + \item \dots hat in diesem Fall nicht geholfen
5.215 + \end{itemize}
5.216 + \item Versuch zur Vermutung: Projekt wurde umbenannt von ``Isac'' in ``isac-jedit'', und das machte build.xml inkonsistent
5.217 + \begin{itemize}
5.218 + \item in build.xml query-replace ``Isac'' in ``isac-jedit''
5.219 + \item TODO?
5.220 + \item
5.221 + \end{itemize}
5.222 + \end{enumerate}
5.223 + \item Wenn: Problem: failed to create tsk or type scalac
5.224 + \begin{enumerate}
5.225 + \item Versuch: Pfad zum Scala bekanntgeben
5.226 + \begin{itemize}
5.227 + \item /usr/local/netbeans-6.9.1/etc/netbeans.conf: netbeans\_default\_options= richtigen Scala-Pfad setzen
5.228 + \item build-impl.xml l\"oschen
5.229 + \item NetBeans neu starten.
5.230 + \end{itemize}
5.231 + \end{enumerate}
5.232 + \item Wenn Fehler: ``/usr/local/isabisac/src/Tools/jEditC/\${project.jEdit}/modes does not exist''
5.233 + \begin{enumerate}
5.234 + \item grep -r "project.jEdit" *
5.235 + \item nbproject/project.properties:project.jEdit=contrib/jEdit
5.236 + \item
5.237 + \item
5.238 +
5.239 + \begin{itemize}
5.240 + \item
5.241 + \begin{itemize}
5.242 + \item
5.243 + \item
5.244 + \item
5.245 + \end{itemize}
5.246 + \item
5.247 + \item
5.248 + \end{itemize}
5.249 + \item
5.250 + \item
5.251 + \end{enumerate}
5.252 + \item
5.253 + \item
5.254 + \end{enumerate}
5.255 + \end{enumerate}
5.256 +$<$ $>$
5.257 +Men\"u $>$ $>$ $>$ $>$ $>$ $>$
5.258 +``Project''-View $>$ rightMouse $>$ $>$ $>$ $>$ $>$
5.259 +\item
5.260 + \begin{enumerate}
5.261 + \item
5.262 + \begin{enumerate}
5.263 + \item
5.264 + \begin{itemize}
5.265 + \item
5.266 + \begin{itemize}
5.267 + \item
5.268 + \item
5.269 + \item
5.270 + \end{itemize}
5.271 + \item
5.272 + \item
5.273 + \end{itemize}
5.274 + \item
5.275 + \item
5.276 + \end{enumerate}
5.277 + \item
5.278 + \item
5.279 + \end{enumerate}
5.280 +\item
5.281 + \begin{enumerate}
5.282 + \item
5.283 + \begin{enumerate}
5.284 + \item
5.285 + \begin{itemize}
5.286 + \item
5.287 + \begin{itemize}
5.288 + \item
5.289 + \item
5.290 + \item
5.291 + \end{itemize}
5.292 + \item
5.293 + \item
5.294 + \end{itemize}
5.295 + \item
5.296 + \item
5.297 + \end{enumerate}
5.298 + \item
5.299 + \item
5.300 + \end{enumerate}
5.301 +\end{enumerate}
5.302 +
5.303 +
5.304 +\section{Implementation der jEdit Komponenten}
5.305 +
5.306 +\subsection{Erstellen des Plugin-Ger\"{u}sts}
5.307 +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.
5.308 +
5.309 +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.
5.310 +
5.311 +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.
5.312 +
5.313 +\subsection{Erzeugung des Plugins}
5.314 +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):
5.315 +\begin{enumerate}
5.316 +\item Das Plugin kann mittels Kommandline folgenderma{\ss}en erstellt werden: \\ \textit{cd ISABELLE\_HOME/src/Tools/isac/jEdit} $\rightarrow$ \textit{ant jar}
5.317 +\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/}
5.318 +\item jEdit ausf\"{u}hren und testen
5.319 +\end{enumerate}
5.320 +
5.321 +\subsection{Verbindung zum Isabelle-Pure Plugin herstellen}
5.322 +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.
5.323 +
5.324 +\begin{figure}
5.325 +\begin{center}
5.326 +\includegraphics[width=100mm]{../fig-jedit-plugins-SD}
5.327 +\end{center}
5.328 +\label{fig-jedit-plugins-SD}
5.329 +\end{figure}
5.330 +
5.331 +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.
5.332 +
5.333 +
5.334 +\begin{enumerate}
5.335 +\item Um den \sisac-Teil im Isabelle-Pure genau abzugrenzen, wurde ein Ordner \textit{Isac} angelegt und ein Testfile \textit{isac.scala} erstellt.
5.336 +\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.
5.337 +\item Nun kann Pure.jar mittels Kommandline erstellt werden: \textit{cd /src/Pure} $\rightarrow$ \textit{../../bin/isabelle env ./build-jars}
5.338 +\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/}
5.339 +\item jEdit ausf\"{u}hren und testen
5.340 +\end{enumerate}
5.341 +Alle die oben angef\"{u}hrten Punkte, sowie das Erzeugen und Kopieren des Plugins selbst, werden vom Script isac\_jedit erledigt.
5.342 +Das Skript kann dem Anhang C entnommen werden.
5.343 +
5.344 +\section{Umsetzung des SD-Parsers}
5.345 +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.
5.346 +
5.347 +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.
5.348 +
5.349 +
5.350 +\chapter{Ausblick: Von SD- zum \isac-Plugin}
5.351 +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.
5.352 +
5.353 +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.
5.354 +
5.355 +\chapter{Zusammenfassung und R\"{u}ckblick}
5.356 +Zusammenfassend wird nun ein \"Uberblick gegeben, welche Milestones erledigt wurden und welche nicht; Details dazu finden sich in Anhang A. %TODO
5.357 +Abschlie{\ss}end gebe ich einen R\"uckblick auf meine pers\"onlichen Erfahrungen aus dieser Bakkalaureats-Arbeit.
5.358 +
5.359 +\section{Zusammenfassung}
5.360 +Folgende Milestones wurden erfolgreich abgeschlossen:
5.361 +\begin{enumerate}
5.362 +\item Relevante Isabelle Komponenten dokumentiert
5.363 +
5.364 +\item Installation der Standard-Komponenten:
5.365 + \begin{itemize}
5.366 + \item Mercurial Versioncontrol
5.367 + \item NetBeans IDE
5.368 + \item Standard Isabelle Bundle
5.369 + \end{itemize}
5.370 +
5.371 +\item Entwicklungsumgebung vom Isabelle-Team kopieren
5.372 + \begin{itemize}
5.373 + \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
5.374 + \item jEdit als NetBeans Projekt definiert
5.375 + \end{itemize}
5.376 +
5.377 +\item Relevante Komponenten implementieren
5.378 + \begin{itemize}
5.379 + \item jEdit Plugin f\"ur SD
5.380 + \item Verbindung des Plugins zu Isabelle
5.381 + \item zugeh\"origen Parser: nur ein Test in SML
5.382 + \end{itemize}
5.383 +\end{enumerate}
5.384 +
5.385 +\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.
5.386 +
5.387 +\paragraph{Voraussetzungen f\"ur k\"unftige Entwicklung} geschaffen:
5.388 +\begin{enumerate}
5.389 +\item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
5.390 +\item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend
5.391 +\item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).
5.392 +\end{enumerate}
5.393 +
5.394 +\section{R\"uckblick}
5.395 +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.
5.396 +
5.397 +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.
5.398 +
5.399 +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.
5.400 +
5.401 +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.
5.402 +
5.403 +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.
5.404 +
5.405 +%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!
5.406 +
5.407 +%\chapter{Milestones und Arbeitsprotokolle}
5.408 +%\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010}
5.409 +%\begin{itemize}
5.410 +%\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010
5.411 +%\item Charakteristika der Programmsprache Scala: beendet am 27.09.2010
5.412 +%\item Scala Actors: beendet am 12.08.2010
5.413 +%\end{itemize}
5.414 +%\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
5.415 +%\hline
5.416 +%Datum & T\"atigkeit & Einheiten \\ \hline
5.417 +%12.07.2010 & Meeting: erste Besprechung und Erkl\"{a}rungen zu Isabelle, Isac und CTPs & 2 \\ \hline
5.418 +%15.07.2010 & Recherche \"{u}ber Isabelle und CTPs & 3 \\ \hline
5.419 +%20.07.2010 & Meeting: Besprechen der grunds\"{a}tzlichen Vorgangsweise und Ziele & 1 \\ \hline
5.420 +%23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline
5.421 +%30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise \"{u}ber Backs 'structured derivations'; Begriffserkl\"{a}rung & 3 \\ \hline
5.422 +%01.08.2010 & Recherche: Buch f\"{u}r Scala & 2 \\ \hline
5.423 +%03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
5.424 +%05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
5.425 +%06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
5.426 +%08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
5.427 +%09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
5.428 +%12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
5.429 +%24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
5.430 +%25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
5.431 +%27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline \hline
5.432 +% & Anzahl der Einheiten & 44 \\
5.433 +%\hline
5.434 +%\end{tabular}
5.435 +%
5.436 +%
5.437 +%\section{Technische Voraussetzungen hergestellt: beendet am 02.08.2010}
5.438 +%\begin{itemize}
5.439 +%\item Isabelle installiert, Filestruktur bekannt: beendet am 02.08.2010
5.440 +%\item Scala in NetBeans eingebunden: beendet am 22.07.2010
5.441 +%\item Mercurial installiert und einrichten des Repositories: beendet am 19.07.2010
5.442 +%\end{itemize}
5.443 +%\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
5.444 +%\hline
5.445 +%Datum & T\"atigkeit & Einheiten \\ \hline
5.446 +%19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
5.447 +%20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
5.448 +%21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
5.449 +%22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
5.450 +%23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline
5.451 +%27.07.2010 & Isabelle-jEdit-Plugin: \"{a}nderungen an der Projektstruktur & 7 \\ \hline
5.452 +%28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
5.453 +%29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
5.454 +%30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung \"{u}ber Erfahrungen mit Filestruktur & 4 \\ \hline
5.455 +%02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
5.456 +% & Anzahl der Einheiten & 60 \\
5.457 +%\hline
5.458 +%\end{tabular}
5.459 +%
5.460 +%\section{NetBeans-Projekt aufgesetzt: beendet am 02.08.2010}
5.461 +%\begin{itemize}
5.462 +%\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: beendet am 02.08.2010
5.463 +%\item jEdit-Plugin: XML-Files f\"{u}r ISAC vorbereitet: beendet am 22.07.2010
5.464 +%\item jEdit-Plugin: Source files geschrieben: beendet am 19.07.2010
5.465 +%\end{itemize}
5.466 +%\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
5.467 +%\hline
5.468 +%Datum & T\"atigkeit & Einheiten \\ \hline
5.469 +%10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
5.470 +%11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
5.471 +%21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
5.472 +%22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten f\"{u}r ISAC & 3 \\ \hline
5.473 +%24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline
5.474 +%26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach L\"{o}sungen & 3 \\ \hline
5.475 +%28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
5.476 +%29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
5.477 +%30.08.2010 & Isabelle-jEdit-Plugin endlich vollst\"{a}ndig lauff\"{a}hig gebracht & 4 \\ \hline
5.478 +%01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
5.479 +%04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline
5.480 +%20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline
5.481 +%22.09.2010 & Meeting: Fortschrittsbericht, kurze Einf\"{u}hrung f\"{u}r Mitstreiter & 3 \\ \hline
5.482 +%
5.483 +%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
5.484 +%30.09.2010 & QN: Start mit \"{u}bersetzten der Sourcefiles & 5 \\ \hline
5.485 +%02.10.2010 & QN: \"{U}bersetzten der Sourcefiles & 6 \\ \hline
5.486 +%04.10.2010 & QN: \"{U}bersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
5.487 +%05.10.2010 & QN: QN vollst\"andig in Scala \"{u}bersetzt, testen & 2 \\ \hline \hline
5.488 +% & Anzahl der Einheiten & 71 \\
5.489 +%\hline
5.490 +%\end{tabular}
5.491 +%
5.492 +%\section{Experimentelle Parser implementiert: beendet am 04.03.2011}
5.493 +%\begin{itemize}
5.494 +%\item Experimente mit dem SideKick-Parser abgeschlossen: beendet am 03.02.2011
5.495 +%\item Verbindung zu Isabelle-Pure hergestellt: beendet am 04.03.2011
5.496 +%\item Implementierung des Scala-Parsers: aufgeschoben
5.497 +%\end{itemize}
5.498 +%\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
5.499 +%\hline
5.500 +%Datum & T\"atigkeit & Einheiten \\ \hline
5.501 +%28.01.2011 & Testen des SideKick-Parsers im Isabelle-Plugin & 2 \\ \hline
5.502 +%29.01.2011 & Leichte Modifikationen des SideKick-Parsers im Isabelle-Plugin & 1 \\ \hline
5.503 +%08.02.2011 & Besprechung zum Abschluss der praktischen Arbeiten & 1 \\ \hline
5.504 +%16.02.2011 & Erstellen des Isabelle-Pur jar-Files & 1 \\ \hline
5.505 +%19.02.2011 & Behebung des Problems mit den Umgebungsvariablen & 1 \\ \hline
5.506 +%03.03.2011 & Erzeugung des Pure.jar Package m\"{o}glich & 2 \\ \hline
5.507 +%04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet & 3 \\ \hline
5.508 +%08.04.2011 & Besprechung: Implementierung des experimentellen Parsers wird nicht mehr durchgef\"{u}hrt & 1 \\ \hline \hline
5.509 +% & Anzahl der Einheiten & 12 \\
5.510 +%\hline
5.511 +%\end{tabular}
5.512 +%
5.513 +%\section{Verfassen der Dokumentation und abschliesende Arbeiten: beendet am TO.DO.2011}
5.514 +%\begin{itemize}
5.515 +%\item Bacc.-Protokoll fertiggestellt: beendet am 01.03.2011
5.516 +%\item Dokumentation: erste Version fertiggestellt: beendet am 28.04.2011
5.517 +%\item Dokumentation abgeschlossen: beendet am TO.DO.2011
5.518 +%\end{itemize}
5.519 +%\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
5.520 +%\hline
5.521 +%Datum & T\"atigkeit & Einheiten \\ \hline
5.522 +%01.03.2011 & Besprechung zum Ablauf der Dokumentationsarbeiten: Protokoll und Dokumentation & 1 \\ \hline
5.523 +%01.03.2011 & Erstellen des Protokolls & 2 \\ \hline
5.524 +%08.03.2011 & Besprechung zur Doku und zur Schnittstelle zu Isabelle-Pure & 1 \\ \hline
5.525 +%17.03.2011 & Dokumentation schreiben & 2 \\ \hline
5.526 +%19.03.2011 & Dokumentation schreiben & 3 \\ \hline
5.527 +%24.04.2011 & Dokumentation schreiben & 2 \\ \hline
5.528 +%25.04.2011 & Dokumentation schreiben & 4 \\ \hline
5.529 +%27.04.2011 & Dokumentation schreiben & 2 \\ \hline
5.530 +%28.04.2011 & Dokumentation: Fertigstellen der ersten Version & 3 \\ \hline \hline
5.531 +% & Anzahl der Einheiten & 20 \\
5.532 +%\hline
5.533 +%\end{tabular}
5.534 +%
5.535 +%\section{Pr\"asentation der Arbeit im IST-Seminar }% am ..(*)...}
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/isac/msteger/bakk-arbeit/master_thesis.bib Tue Jun 28 17:09:05 2011 +0200
6.3 @@ -0,0 +1,162 @@
6.4 +% Add your bibtex entries
6.5 +@inproceedings{Aspinall:2007:FIP:1420412.1420429,
6.6 + author = {Aspinall, David and L\"{u}th, Christoph and Winterstein, Daniel},
6.7 + title = {A Framework for Interactive Proof},
6.8 + booktitle = {Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference},
6.9 + series = {Calculemus '07 / MKM '07},
6.10 + year = {2007},
6.11 + isbn = {978-3-540-73083-5},
6.12 + location = {Hagenberg, Austria},
6.13 + pages = {161--175},
6.14 + numpages = {15},
6.15 + url = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
6.16 + doi = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
6.17 + acmid = {1420429},
6.18 + publisher = {Springer-Verlag},
6.19 + address = {Berlin, Heidelberg},
6.20 +}
6.21 +
6.22 +@Book{armstrong:erlang96,
6.23 + author = {Armstrong, Joe and others},
6.24 + title = {Concurrent Programming in Erlang},
6.25 + publisher = {Prentice Hall},
6.26 + year = {1996}
6.27 +}
6.28 +
6.29 +@TechReport{odersky:scala06,
6.30 + author = {Odersky, Martin and others},
6.31 + title = {An Overview of the Scala Programming Language},
6.32 + institution = {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)},
6.33 + year = {2006},
6.34 + type = {Technical Report LAMP-REPORT-2006-001},
6.35 + address = {1015 Lausanne, Switzerland},
6.36 + note = {Second Edition},
6.37 + annote = {http://www.scala-lang.org/sites/default/files/linuxsoft_archives/docu/files/ScalaOverview.pdf}
6.38 +}
6.39 +
6.40 +@article{Haller:2009:SAU:1496391.1496422,
6.41 + author = {Haller, Philipp and Odersky, Martin},
6.42 + title = {Scala Actors: Unifying thread-based and event-based programming},
6.43 + journal = {Theor. Comput. Sci.},
6.44 + volume = {410},
6.45 + issue = {2-3},
6.46 + month = {February},
6.47 + year = {2009},
6.48 + issn = {0304-3975},
6.49 + pages = {202--220},
6.50 + numpages = {19},
6.51 + url = {http://portal.acm.org/citation.cfm?id=1496391.1496422},
6.52 + doi = {10.1016/j.tcs.2008.09.019},
6.53 + acmid = {1496422},
6.54 + publisher = {Elsevier Science Publishers Ltd.},
6.55 + address = {Essex, UK},
6.56 + keywords = {Actors, Concurrent programming, Events, Threads},
6.57 +}
6.58 +
6.59 +@InProceedings{scala:jmlc06,
6.60 + author = {Philipp Haller and Martin Odersky},
6.61 + title = {Event-Based Programming without Inversion of Control},
6.62 + booktitle = {Proc. Joint Modular Languages Conference},
6.63 + year = 2006,
6.64 + series = {Springer LNCS}
6.65 +}
6.66 +
6.67 +
6.68 +@InProceedings{makarius:isa-scala-jedit,
6.69 + author = {Makarius Wenzel},
6.70 + title = {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
6.71 + booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
6.72 + year = {2010},
6.73 + editor = {C. Sacerdoti Coen and D. Aspinall},
6.74 + address = {Edinburgh, Scotland},
6.75 + month = {July},
6.76 + organization = {FLOC 2010 Satellite Workshop},
6.77 + note = {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
6.78 +}
6.79 +
6.80 +@Book{db:dom-eng,
6.81 + author = {Bj{\o}rner, Dines},
6.82 + title = {Domain Engineering. Technology Management, Research and Engineering},
6.83 + publisher = {JAIST Press},
6.84 + year = {2009},
6.85 + month = {Feb},
6.86 + series = {COE Research Monograph Series},
6.87 + volume = {4},
6.88 + address = {Nomi, Japan}
6.89 +}
6.90 +
6.91 +@inproceedings{Haftmann-Nipkow:2010:code,
6.92 + author = {Florian Haftmann and Tobias Nipkow},
6.93 + title = {Code Generation via Higher-Order Rewrite Systems},
6.94 + booktitle = {Functional and Logic Programming, 10th International
6.95 +Symposium: {FLOPS} 2010},
6.96 + year = {2010},
6.97 + publisher = {Springer},
6.98 + series = {Lecture Notes in Computer Science},
6.99 + volume = {6009}
6.100 +}
6.101 +
6.102 +@Manual{coq1999,
6.103 + title = {The Coq Proof Assistant},
6.104 + author = {Barras, B. and others},
6.105 + organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},
6.106 + month = {July},
6.107 + year = {1999},
6.108 + pnote={},status={cited},source={mkm01.caprotti},location={}
6.109 +}
6.110 +
6.111 +@Book{meta-ML,
6.112 + author = {Gordon,M. and Milner,R. and Wadsworth,C. P.},
6.113 + title = {Edinburgh LCF: A Mechanised Logic of Computation},
6.114 + publisher = { Springer-Verlag},
6.115 + year = {1979},
6.116 + volume = {78},
6.117 + series = {Lecture Notes in Computer Science}
6.118 +}
6.119 +
6.120 +@book{Paulson:Isa94,
6.121 + title={Isabelle: a generic theorem prover},
6.122 + author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994},
6.123 + volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={},
6.124 + note={With contributions by Topias Nipkow},
6.125 + status={},source={},location={-}
6.126 + }
6.127 +
6.128 +@Book{pl:milner97,
6.129 + author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
6.130 + title = {The Definition of Standard ML (Revised)},
6.131 + publisher = {The MIT Press},
6.132 + year = 1997,
6.133 + address = {Cambridge, London},
6.134 + annote = {97bok375}
6.135 +}
6.136 +
6.137 +@Article{back-grundy-wright-98,
6.138 + author = {Back, Ralph and Grundy, Jim and von Wright, Joakim},
6.139 + title = {Structured Calculational Proof},
6.140 + journal = {Formal Aspects of Computing},
6.141 + year = {1998},
6.142 + number = {9},
6.143 + pages = {469-483}
6.144 +}
6.145 +
6.146 +@Manual{isar-impl,
6.147 + title = {The {Isabelle/Isar} Implementation},
6.148 + author = {Makarius Wenzel},
6.149 + month = {April 19},
6.150 + year = {2009},
6.151 + note = {With contributions by Florian Haftmann and Larry Paulson}
6.152 +}
6.153 +
6.154 +@InProceedings{wenzel:isar,
6.155 + author = {Wenzel, Markus},
6.156 + title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
6.157 + booktitle = {Theorem Proving in Higher Order Logics},
6.158 + year = {1999},
6.159 + editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
6.160 + series = {LNCS 1690},
6.161 + organization = {12th International Conference TPHOLs'99},
6.162 + publisher = {Springer}
6.163 +}
6.164 +
6.165 +
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-acknowl.tex Tue Jun 28 17:09:05 2011 +0200
7.3 @@ -0,0 +1,45 @@
7.4 +%\begin{changemargin}{1.5cm}{1.5cm}
7.5 +
7.6 +%\chapter*{Acknowledgements}
7.7 +%\addcontentsline{toc}{chapter}{Acknowledgements}
7.8 +
7.9 +
7.10 +
7.11 +\begin{center}
7.12 +{\Large\bfseries Acknowledgements}
7.13 +\end{center}
7.14 +%\vspace*{3mm}
7.15 +
7.16 +\begin{changemargin}{1.5cm}{1.5cm}
7.17 +I would like to thank ...
7.18 +
7.19 +\begin{flushright}
7.20 +your name \\ {\small place, county, date}
7.21 +\end{flushright}
7.22 +\end{changemargin}
7.23 +
7.24 +\selectlanguage{austrian}
7.25 +
7.26 +\vspace*{5mm}
7.27 +
7.28 +\begin{center}
7.29 +{\Large\bfseries Danksagung}
7.30 +\end{center}
7.31 +%\vspace*{0mm}
7.32 +
7.33 +\begin{changemargin}{1.5cm}{1.5cm}
7.34 +Ich möchte mich herzlich bei allen bedanken, die ...
7.35 +
7.36 +\begin{flushright}
7.37 +Dein Name \\ {\small Ort, Land, Datum}
7.38 +\end{flushright}
7.39 +\end{changemargin}
7.40 +
7.41 +\selectlanguage{english}
7.42 +
7.43 +
7.44 +
7.45 +
7.46 +
7.47 +
7.48 +
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-appendix.tex Tue Jun 28 17:09:05 2011 +0200
8.3 @@ -0,0 +1,339 @@
8.4 +\chapter{Milestones und Arbeitsprotokolle}\label{milestones} %\ref doesnt work outside this file ?!?
8.5 +\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010}
8.6 +\begin{itemize}
8.7 +\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010
8.8 +\item Charakteristika der Programmsprache Scala: beendet am 27.09.2010
8.9 +\item Scala Actors: beendet am 12.08.2010
8.10 +\end{itemize}
8.11 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
8.12 +\hline
8.13 +Datum & T\"atigkeit & Einheiten \\ \hline
8.14 +12.07.2010 & Meeting: erste Besprechung und Erkl\"{a}rungen zu Isabelle, Isac und CTPs & 2 \\ \hline
8.15 +15.07.2010 & Recherche \"{u}ber Isabelle und CTPs & 3 \\ \hline
8.16 +20.07.2010 & Meeting: Besprechen der grunds\"{a}tzlichen Vorgangsweise und Ziele & 1 \\ \hline
8.17 +23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline
8.18 +30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise \"{u}ber Backs 'structured derivations'; Begriffserkl\"{a}rung & 3 \\ \hline
8.19 +01.08.2010 & Recherche: Buch f\"{u}r Scala & 2 \\ \hline
8.20 +03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
8.21 +05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
8.22 +06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
8.23 +08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
8.24 +09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
8.25 +12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
8.26 +24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
8.27 +25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
8.28 +27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline \hline
8.29 + & Anzahl der Einheiten & 44 \\
8.30 +\hline
8.31 +\end{tabular}
8.32 +
8.33 +
8.34 +\section{Technische Voraussetzungen hergestellt: beendet am 02.08.2010}
8.35 +\begin{itemize}
8.36 +\item Isabelle installiert, Filestruktur bekannt: beendet am 02.08.2010
8.37 +\item Scala in NetBeans eingebunden: beendet am 22.07.2010
8.38 +\item Mercurial installiert und einrichten des Repositories: beendet am 19.07.2010
8.39 +\end{itemize}
8.40 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
8.41 +\hline
8.42 +Datum & T\"atigkeit & Einheiten \\ \hline
8.43 +19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
8.44 +20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
8.45 +21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
8.46 +22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
8.47 +23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline
8.48 +27.07.2010 & Isabelle-jEdit-Plugin: \"{a}nderungen an der Projektstruktur & 7 \\ \hline
8.49 +28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
8.50 +29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
8.51 +30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung \"{u}ber Erfahrungen mit Filestruktur & 4 \\ \hline
8.52 +02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
8.53 + & Anzahl der Einheiten & 60 \\
8.54 +\hline
8.55 +\end{tabular}
8.56 +
8.57 +\section{NetBeans-Projekt aufgesetzt: beendet am 02.08.2010}
8.58 +\begin{itemize}
8.59 +\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: beendet am 02.08.2010
8.60 +\item jEdit-Plugin: XML-Files f\"{u}r ISAC vorbereitet: beendet am 22.07.2010
8.61 +\item jEdit-Plugin: Source files geschrieben: beendet am 19.07.2010
8.62 +\end{itemize}
8.63 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
8.64 +\hline
8.65 +Datum & T\"atigkeit & Einheiten \\ \hline
8.66 +10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
8.67 +11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
8.68 +21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
8.69 +22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten f\"{u}r ISAC & 3 \\ \hline
8.70 +24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline
8.71 +26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach L\"{o}sungen & 3 \\ \hline
8.72 +28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
8.73 +29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
8.74 +30.08.2010 & Isabelle-jEdit-Plugin endlich vollst\"{a}ndig lauff\"{a}hig gebracht & 4 \\ \hline
8.75 +01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
8.76 +04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline
8.77 +20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline
8.78 +22.09.2010 & Meeting: Fortschrittsbericht, kurze Einf\"{u}hrung f\"{u}r Mitstreiter & 3 \\ \hline
8.79 +
8.80 +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
8.81 +30.09.2010 & QN: Start mit \"{u}bersetzten der Sourcefiles & 5 \\ \hline
8.82 +02.10.2010 & QN: \"{U}bersetzten der Sourcefiles & 6 \\ \hline
8.83 +04.10.2010 & QN: \"{U}bersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
8.84 +05.10.2010 & QN: QN vollst\"andig in Scala \"{u}bersetzt, testen & 2 \\ \hline \hline
8.85 + & Anzahl der Einheiten & 71 \\
8.86 +\hline
8.87 +\end{tabular}
8.88 +
8.89 +\section{Experimentelle Parser implementiert: beendet am 04.03.2011}
8.90 +\begin{itemize}
8.91 +\item Experimente mit dem SideKick-Parser abgeschlossen: beendet am 03.02.2011
8.92 +\item Verbindung zu Isabelle-Pure hergestellt: beendet am 04.03.2011
8.93 +\item Implementierung des Scala-Parsers: aufgeschoben
8.94 +\end{itemize}
8.95 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
8.96 +\hline
8.97 +Datum & T\"atigkeit & Einheiten \\ \hline
8.98 +28.01.2011 & Testen des SideKick-Parsers im Isabelle-Plugin & 2 \\ \hline
8.99 +29.01.2011 & Leichte Modifikationen des SideKick-Parsers im Isabelle-Plugin & 1 \\ \hline
8.100 +08.02.2011 & Besprechung zum Abschluss der praktischen Arbeiten & 1 \\ \hline
8.101 +16.02.2011 & Erstellen des Isabelle-Pur jar-Files & 1 \\ \hline
8.102 +19.02.2011 & Behebung des Problems mit den Umgebungsvariablen & 1 \\ \hline
8.103 +03.03.2011 & Erzeugung des Pure.jar Package m\"{o}glich & 2 \\ \hline
8.104 +04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet & 3 \\ \hline
8.105 +08.04.2011 & Besprechung: Implementierung des experimentellen Parsers wird nicht mehr durchgef\"{u}hrt & 1 \\ \hline \hline
8.106 + & Anzahl der Einheiten & 12 \\
8.107 +\hline
8.108 +\end{tabular}
8.109 +
8.110 +\section{Verfassen der Dokumentation und abschliesende Arbeiten: beendet am TO.DO.2011}
8.111 +\begin{itemize}
8.112 +\item Bacc.-Protokoll fertiggestellt: beendet am 01.03.2011
8.113 +\item Dokumentation: erste Version fertiggestellt: beendet am 28.04.2011
8.114 +\item Dokumentation abgeschlossen: beendet am TO.DO.2011
8.115 +\end{itemize}
8.116 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
8.117 +\hline
8.118 +Datum & T\"atigkeit & Einheiten \\ \hline
8.119 +01.03.2011 & Besprechung zum Ablauf der Dokumentationsarbeiten: Protokoll und Dokumentation & 1 \\ \hline
8.120 +01.03.2011 & Erstellen des Protokolls & 2 \\ \hline
8.121 +08.03.2011 & Besprechung zur Doku und zur Schnittstelle zu Isabelle-Pure & 1 \\ \hline
8.122 +17.03.2011 & Dokumentation schreiben & 2 \\ \hline
8.123 +19.03.2011 & Dokumentation schreiben & 3 \\ \hline
8.124 +24.04.2011 & Dokumentation schreiben & 2 \\ \hline
8.125 +25.04.2011 & Dokumentation schreiben & 4 \\ \hline
8.126 +27.04.2011 & Dokumentation schreiben & 2 \\ \hline
8.127 +28.04.2011 & Dokumentation: Fertigstellen der ersten Version & 3 \\ \hline \hline
8.128 + & Anzahl der Einheiten & 20 \\
8.129 +\hline
8.130 +\end{tabular}
8.131 +
8.132 +\section{Pr\"asentation der Arbeit im IST-Seminar: beendet am 21.06.2011}
8.133 +\begin{itemize}
8.134 +\item Pr\"asentation fertiggestellt: beendet am 19.06.2011
8.135 +\item Pr\"asentation: abgehalten am 21.06.2011
8.136 +\end{itemize}
8.137 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
8.138 +\hline
8.139 +Datum & T\"atigkeit & Einheiten \\ \hline
8.140 +06.06.2011 & Planung der Pr\"asentation & 2 \\ \hline
8.141 +16.06.2011 & Verfassen der Pr\"asentation & 2 \\ \hline
8.142 +18.06.2011 & Verfassen der Pr\"asentation & 3 \\ \hline
8.143 +19.06.2011 & Pr\"asentation: Feinschliff & 2 \\ \hline
8.144 +20.06.2011 & Vorbereiten der Pr\"asentation& 3 \\ \hline
8.145 +21.06.2011 & Abhaltung und nachfolgende Diskussion & 1 \\ \hline \hline
8.146 + & Anzahl der Einheiten & 13 \\
8.147 + \hline
8.148 +\end{tabular}
8.149 +
8.150 +\chapter{Filestruktur Isabelle}
8.151 +\section{jar-Packete}
8.152 +\textbf{----- for "isabelle jedit \&"; contained in Isabelle\_bundle} \\
8.153 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar \\
8.154 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar \\
8.155 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar \\
8.156 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar \\
8.157 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \\
8.158 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar \\
8.159 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar \\
8.160 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar \\
8.161 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar \\
8.162 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar \\
8.163 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar \\
8.164 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar \\
8.165 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar \\
8.166 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar \\
8.167 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar \\
8.168 +\textbf{----- scala system; contained in Isabelle\_bundle} \\
8.169 +./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar \\
8.170 +./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar \\
8.171 +./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar \\
8.172 +./contrib/scala-2.8.1.final/lib/scala-compiler.jar \\
8.173 +./contrib/scala-2.8.1.final/lib/scalap.jar \\
8.174 +./contrib/scala-2.8.1.final/lib/scala-swing.jar \\
8.175 +./contrib/scala-2.8.1.final/lib/scala-library.jar \\
8.176 +./contrib/scala-2.8.1.final/lib/jline.jar \\
8.177 +./contrib/scala-2.8.1.final/lib/scala-dbc.jar \\
8.178 +./contrib/scala-2.8.1.final/src/scala-library-src.jar \\
8.179 +./contrib/scala-2.8.1.final/src/scala-swing-src.jar \\
8.180 +./contrib/scala-2.8.1.final/src/scala-compiler-src.jar \\
8.181 +./contrib/scala-2.8.1.final/src/scala-dbc-src.jar \\
8.182 +./contrib/scala-2.8.1.final/src/sbaz-src.jar \\
8.183 +\textbf{----- Isars entry to SML from Scala-layer; } \\
8.184 +\textit{created according to 4.3.\#3 }\\
8.185 +./lib/classes/isabelle-scala.jar \\
8.186 +./lib/classes/Pure.jar \\\\
8.187 +\textit{\textbf{===== all below for NetBeans}} \\\\
8.188 +\textbf{----- standard Isabelle, started by $<RUN>$ in NetBeans} \\
8.189 + \textit{description in 2.2.2} \\
8.190 +./src/Tools/jEdit/dist/jars/jedit.jar \\
8.191 +./src/Tools/jEdit/dist/jars/SideKick.jar \\
8.192 +./src/Tools/jEdit/dist/jars/Console.jar \\
8.193 +./src/Tools/jEdit/dist/jars/Pure.jar \\
8.194 +./src/Tools/jEdit/dist/jars/scala-compiler.jar \\
8.195 +./src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar \\
8.196 +./src/Tools/jEdit/dist/jars/cobra.jar \\
8.197 +./src/Tools/jEdit/dist/jars/js.jar \\
8.198 +./src/Tools/jEdit/dist/jars/Hyperlinks.jar \\
8.199 +./src/Tools/jEdit/dist/jars/scala-swing.jar \\
8.200 +./src/Tools/jEdit/dist/jars/scala-library.jar \\
8.201 +./src/Tools/jEdit/dist/jars/ErrorList.jar \\
8.202 +\textbf{----- source of jEdit, required for $<DEBUG>$ in NetBeans; \\}
8.203 + adapted from NetBeans' webpages, \\
8.204 + \textit{description in 2.2.3.\#5} \\
8.205 +./src/Tools/jEditC/contrib/jEdit/build/jars/SideKick.jar \\
8.206 +./src/Tools/jEditC/contrib/jEdit/build/jars/Console.jar \\
8.207 +./src/Tools/jEditC/contrib/jEdit/build/jars/Pure.jar \\
8.208 +./src/Tools/jEditC/contrib/jEdit/build/jars/Isac.jar \\
8.209 +./src/Tools/jEditC/contrib/jEdit/build/jars/QuickNPScala.jar \\
8.210 +./src/Tools/jEditC/contrib/jEdit/build/jars/scala-compiler.jar \\
8.211 +./src/Tools/jEditC/contrib/jEdit/build/jars/Isabelle-jEdit.jar \\
8.212 +./src/Tools/jEditC/contrib/jEdit/build/jars/cobra.jar \\
8.213 +./src/Tools/jEditC/contrib/jEdit/build/jars/js.jar \\
8.214 +./src/Tools/jEditC/contrib/jEdit/build/jars/Hyperlinks.jar \\
8.215 +./src/Tools/jEditC/contrib/jEdit/build/jars/scala-swing.jar \\
8.216 +./src/Tools/jEditC/contrib/jEdit/build/jars/scala-library.jar \\
8.217 +./src/Tools/jEditC/contrib/jEdit/build/jars/ErrorList.jar \\
8.218 +./src/Tools/jEditC/contrib/jEdit/build/jEdit.jar \\
8.219 +\textbf{----- demo plugin, started by $<RUN>$ in NetBeans \\}
8.220 + \textit{description in 2.2.3.\#4} \\
8.221 +./src/Tools/jEditC/dist/jars/SideKick.jar \\
8.222 +./src/Tools/jEditC/dist/jars/Console.jar \\
8.223 +./src/Tools/jEditC/dist/jars/Pure.jar \\
8.224 +./src/Tools/jEditC/dist/jars/Isac.jar \\
8.225 +./src/Tools/jEditC/dist/jars/scala-compiler.jar \\
8.226 +./src/Tools/jEditC/dist/jars/cobra.jar \\
8.227 +./src/Tools/jEditC/dist/jars/js.jar \\
8.228 +./src/Tools/jEditC/dist/jars/Hyperlinks.jar \\
8.229 +./src/Tools/jEditC/dist/jars/scala-swing.jar \\
8.230 +./src/Tools/jEditC/dist/jars/scala-library.jar \\
8.231 +./src/Tools/jEditC/dist/jars/ErrorList.jar \\
8.232 +
8.233 +\section{Scala-Files: Isabelle-Pure}
8.234 +\textbf{General:}\\
8.235 +./src/Pure/General/xml.scala\\
8.236 +./src/Pure/General/linear\_set.scala\\
8.237 +./src/Pure/General/symbol.scala\\
8.238 +./src/Pure/General/exn.scala\\
8.239 +./src/Pure/General/position.scala\\
8.240 +./src/Pure/General/scan.scala\\
8.241 +./src/Pure/General/xml\_data.scala\\
8.242 +./src/Pure/General/yxml.scala\\
8.243 +./src/Pure/General/markup.scala\\
8.244 +./src/Pure/General/sha1.scala\\
8.245 +./src/Pure/General/timing.scala\\
8.246 +./src/Pure/General/pretty.scala\\
8.247 +\textbf{Concurent:}\\
8.248 +./src/Pure/Concurrent/volatile.scala\\
8.249 +./src/Pure/Concurrent/future.scala\\
8.250 +./src/Pure/Concurrent/simple\_thread.scala\\
8.251 +\textbf{Thy:}\\
8.252 +./src/Pure/Thy/html.scala\\
8.253 +./src/Pure/Thy/completion.scala\\
8.254 +./src/Pure/Thy/thy\_header.scala\\
8.255 +./src/Pure/Thy/thy\_syntax.scala\\
8.256 +./src/Pure/Isac/isac.scala\\
8.257 +./src/Pure/library.scala\\
8.258 +\textbf{Isar:}\\
8.259 +./src/Pure/Isar/keyword.scala\\
8.260 +./src/Pure/Isar/outer\_syntax.scala\\
8.261 +./src/Pure/Isar/token.scala\\
8.262 +./src/Pure/Isar/parse.scala\\
8.263 +\textbf{Isac:}\\
8.264 +\textit{./src/Pure/Isac/isac.scala}\\
8.265 +\textbf{System:}\\
8.266 +./src/Pure/System/gui\_setup.scala\\
8.267 +./src/Pure/System/isabelle\_system.scala\\
8.268 +./src/Pure/System/swing\_thread.scala\\
8.269 +./src/Pure/System/download.scala\\
8.270 +./src/Pure/System/session\_manager.scala\\
8.271 +./src/Pure/System/standard\_system.scala\\
8.272 +./src/Pure/System/isabelle\_syntax.scala\\
8.273 +./src/Pure/System/session.scala\\
8.274 +./src/Pure/System/platform.scala\\
8.275 +./src/Pure/System/cygwin.scala\\
8.276 +./src/Pure/System/event\_bus.scala\\
8.277 +./src/Pure/System/isabelle\_process.scala\\
8.278 +\textbf{PIDE}\\
8.279 +./src/Pure/PIDE/document.scala\\
8.280 +./src/Pure/PIDE/markup\_tree.scala\\
8.281 +./src/Pure/PIDE/text.scala\\
8.282 +./src/Pure/PIDE/command.scala\\
8.283 +./src/Pure/PIDE/isar\_document.scala \\
8.284 +
8.285 +
8.286 +\chapter{Das Skript \textit{isac\_jedit}}
8.287 +
8.288 +\textit{
8.289 +\#$!$/usr/bin/env bash
8.290 +cd src/Pure/ \\
8.291 +echo "Building Pure.jar" \\
8.292 +../../bin/isabelle env ./build-jars \\
8.293 +echo "copying Pure.jar to contrib/jedit" \\
8.294 +cp ../../lib/classes/Pure.jar ../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ \\
8.295 +echo "Building Isac.jar" \\
8.296 +cd /home/gadei/isac/isa/src/Tools/jEditC \\
8.297 +ant jar \\
8.298 +cd /home/gadei/isac/isa/src/Pure/ \\
8.299 +echo "copying Isac.jar to contrib/jedit" \\
8.300 +cp ../Tools/jEditC/contrib/jEdit/build/jars/Isac.jar ../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ \\
8.301 +echo "Done!" \\
8.302 +}
8.303 +
8.304 +\chapter{Filestruktur f\"ur die Entwicklung des SD-Plugins}
8.305 +
8.306 +build.xml\\
8.307 +makedist\\
8.308 +manifest.mf\\
8.309 +README\_BUILD\\
8.310 +\textbf{build/*}\\
8.311 +\textbf{contrib/*}\\
8.312 +\textbf{dist/*}\\
8.313 +\textbf{plugin/}build.xml\\
8.314 +\textbf{plugin/}changes40.txt\\
8.315 +\textbf{plugin/}changes42.txt\\
8.316 +\textbf{plugin/}description.html\\
8.317 +\textbf{plugin/}IsacActions.java\\
8.318 +\textbf{plugin/}Isac.iml\\
8.319 +\textbf{plugin/}Isac.java\\
8.320 +\textbf{plugin/}IsacOptionPane.java\\
8.321 +\textbf{plugin/}IsacPlugin.java\\
8.322 +\textbf{plugin/}IsacTextArea.java\\
8.323 +\textbf{plugin/}IsacToolPanel.java\\
8.324 +\textbf{plugin/}plugin\\
8.325 +\textbf{plugin/}README.txt\\
8.326 +\textbf{nbproject/*}\\
8.327 +\textbf{src/}actions.xml\\
8.328 +\textbf{src/}changes40.txt\\
8.329 +\textbf{src/}changes42.txt\\
8.330 +\textbf{src/}description.html\\
8.331 +\textbf{src/}dockables.xml\\
8.332 +\textit{\textbf{src/}IsacActions.scala\\}
8.333 +\textbf{src/}Isac.iml\\
8.334 +\textit{\textbf{src/}IsacOptionPane.scala\\}
8.335 +\textit{\textbf{src/}IsacPlugin.scala\\}
8.336 +\textbf{src/}Isac.props\\
8.337 +\textit{\textbf{src/}Isac.scala\\}
8.338 +\textit{\textbf{src/}IsacTextArea.scala\\}
8.339 +\textit{\textbf{src/}IsacToolPanel.scala\\}
8.340 +\textbf{src/}manifest.mf\\
8.341 +\textbf{src/}README.txt\\
8.342 +\textbf{src/}users-guide.xml \\
8.343 \ No newline at end of file
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-biblio.tex Tue Jun 28 17:09:05 2011 +0200
9.3 @@ -0,0 +1,15 @@
9.4 +{
9.5 +
9.6 +\bibliographystyle{plain}
9.7 +
9.8 +
9.9 +% the names of the bib files used
9.10 +
9.11 +\phantomsection
9.12 +\addcontentsline{toc}{chapter}{Bibliography}
9.13 +\bibliography{master_thesis.bib}
9.14 +%\bibliography{../master_thesis.bib}
9.15 +
9.16 +}
9.17 +
9.18 +
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-conclusion.tex Tue Jun 28 17:09:05 2011 +0200
10.3 @@ -0,0 +1,2 @@
10.4 +\chapter{Concluding Remarks}
10.5 +...
10.6 \ No newline at end of file
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-contents.tex Tue Jun 28 17:09:05 2011 +0200
11.3 @@ -0,0 +1,24 @@
11.4 +{
11.5 +\setlength{\parskip}{3pt plus 3pt minus 3pt} % compact table of contents
11.6 +
11.7 +\tableofcontents
11.8 +
11.9 +\listoffigures
11.10 +%\addcontentsline{toc}{chapter}{List of Figures}
11.11 +
11.12 +{
11.13 +% format sections to chapters for this scope
11.14 +\titleformat{\section}{\bf\huge}{\thesection\quad}{0em}{}
11.15 +\titlespacing*{\section}{0em}{-2em}{1.5em}
11.16 +\def\chapter*#1{\section*{#1}}
11.17 +
11.18 +\vspace*{20mm}
11.19 +\listoftables
11.20 +%\addcontentsline{toc}{chapter}{List of Tables}
11.21 +
11.22 +\vspace*{20mm}
11.23 +\lstlistoflistings
11.24 +%\addcontentsline{toc}{chapter}{List of Listings}
11.25 +}
11.26 +}
11.27 +
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-intro.tex Tue Jun 28 17:09:05 2011 +0200
12.3 @@ -0,0 +1,7 @@
12.4 +\chapter{Einf\"{u}hrung}
12.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.
12.6 +
12.7 +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.
12.8 +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.
12.9 +
12.10 +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.
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-macros.tex Tue Jun 28 17:09:05 2011 +0200
13.3 @@ -0,0 +1,67 @@
13.4 +% macros and definitions
13.5 +
13.6 +\newcommand\fname{\begingroup \smaller\urlstyle{tt}\Url}
13.7 +
13.8 +\newcommand\vname{\begingroup \smaller\urlstyle{tt}\Url}
13.9 +
13.10 +
13.11 +% for class names, define our own url style
13.12 +
13.13 +\makeatletter % protect @ names
13.14 +
13.15 +% \url@letstyle: New URL sty to premit break at any letters.
13.16 +% Based on \url@ttstyle
13.17 +
13.18 +\def\Url@letdo{% style assignments for tt fonts or T1 encoding
13.19 +\def\UrlBreaks{\do\a\do\b\do\c\do\d\do\e\do\f\do\g\do\h\do\i\do\j\do\k\do\l%
13.20 + \do\m\do\n\do\o\do\p\do\q\do\r\do\s\do\t\do\u\do\v\do\w\do\x%
13.21 + \do\y\do\z%
13.22 + \do\A\do\B\do\C\do\D\do\E\do\F\do\G\do\H\do\I\do\J\do\K\do\L%
13.23 + \do\M\do\N\do\O\do\P\do\Q\do\R\do\S\do\T\do\U\do\V\do\W\do\X%
13.24 + \do\Y\do\Z%
13.25 +}%
13.26 +\def\UrlBigBreaks{\do\.\do\@\do\\\do\/\do\!\do\_\do\|\do\%\do\;\do\>\do\]%
13.27 + \do\)\do\,\do\?\do\'\do\+\do\=\do\#\do\:\do@url@hyp}%
13.28 +\def\UrlNoBreaks{\do\(\do\[\do\{\do\<}% (unnecessary)
13.29 +\def\UrlSpecials{\do\ {\ }}%
13.30 +\def\UrlOrds{\do\*\do\-\do\~}% any ordinary characters that aren't usually
13.31 +\Urlmuskip = 0mu plus 1mu%
13.32 +}
13.33 +
13.34 +\def\url@letstyle{%
13.35 +\@ifundefined{selectfont}{\def\UrlFont{\sf}}{\def\UrlFont{\sffamily}}\Url@letdo
13.36 +}
13.37 +
13.38 +\makeatother % unprotect @ names
13.39 +
13.40 +
13.41 +\newcommand\cname{\begingroup \smaller\urlstyle{let}\Url}
13.42 +
13.43 +
13.44 +\newcommand{\imgcredit}[1]
13.45 +{%
13.46 +\small
13.47 +[#1]
13.48 +}
13.49 +
13.50 +
13.51 +\newcommand{\chapquote}[2]
13.52 +{%
13.53 +\begin{quote}
13.54 +\emph{%
13.55 +``#1''%
13.56 +}%
13.57 +\begin{flushright}
13.58 +{\scriptsize \sffamily [#2]}%
13.59 +\end{flushright}
13.60 +\end{quote}
13.61 +}
13.62 +
13.63 +
13.64 +% \urlfootnote{url}{day}{month}{year}
13.65 +\newcommand{\murlfootnote}[4]{\footnote{\url{{#1}} (last visit {#4}-{#3}-{#2})}}
13.66 +\newcommand{\murlfootnotebreak}[4]{\footnote{\url{{#1}}\\ \hspace*{6mm}(last visit {#4}-{#3}-{#2})}}
13.67 +
13.68 +% change margin command
13.69 +\def\changemargin#1#2{\list{}{\rightmargin#2\leftmargin#1}\item[]}
13.70 +\let\endchangemargin=\endlist
13.71 \ No newline at end of file
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-preamble.tex Tue Jun 28 17:09:05 2011 +0200
14.3 @@ -0,0 +1,183 @@
14.4 +\usepackage[ % set page and margin sizes
14.5 + a4paper,
14.6 + twoside=false,
14.7 + top=10mm,
14.8 + bottom=10mm,
14.9 + left=20mm,
14.10 + right=20mm,
14.11 + bindingoffset=10mm,
14.12 + head=10mm,
14.13 + foot=10mm,
14.14 + headsep=10mm,
14.15 + footskip=10mm,
14.16 + includeheadfoot,
14.17 +]{geometry}
14.18 +
14.19 +\usepackage{times} % use PostScript fonts
14.20 +%\usepackage{ngerman} % causes ! Illegal parameter number in definition of \grmn@originalTeX. <to be read again> \penalty l.53 \selectlanguage{austrian}
14.21 +\usepackage{relsize} % relative font sizes \smaller \larger
14.22 +
14.23 +\usepackage[iso-8859-1]{inputenx} % so can use Umlaut chars �, �
14.24 +
14.25 +\usepackage{textcomp} % symbols such as \texttimes and \texteuro
14.26 +
14.27 +\usepackage[bf]{titlesec}
14.28 +% format chapter captions (vorher \Huge)
14.29 +\titleformat{\chapter}{\bf\huge}{\thechapter\quad}{0em}{}
14.30 +\titlespacing*{\chapter}{0em}{-2em}{1.5em}
14.31 +
14.32 +% use caption and subfig (caption2 and subfigure are now obsolete)
14.33 +\usepackage[
14.34 + position=bottom,
14.35 + margin=1cm,
14.36 + font=small,
14.37 + labelfont={bf,sf},
14.38 + format=hang,
14.39 + indention=0mm,
14.40 +]{caption,subfig}
14.41 +
14.42 +\captionsetup[subfigure]{
14.43 + margin=0pt,
14.44 + parskip=0pt,
14.45 + hangindent=0pt,
14.46 + indention=0pt,
14.47 + singlelinecheck=true,
14.48 +}
14.49 +
14.50 +
14.51 +
14.52 +% fancyhdr to make nice headers and footers
14.53 +% and deal with long chapter names
14.54 +
14.55 +\usepackage{fancyhdr} % headers and footers
14.56 +\pagestyle{fancy} % must call to set defaults before redefining
14.57 +
14.58 +\renewcommand{\headrulewidth}{0mm}
14.59 +\renewcommand{\footrulewidth}{0mm}
14.60 +\fancyhf{}
14.61 +
14.62 +\fancyhead[R]{\thepage}
14.63 +
14.64 +\fancyhead[L]{
14.65 + \parbox[t]{0.8\textwidth}{\nouppercase{\leftmark}}
14.66 +}
14.67 +
14.68 +
14.69 +% \usepackage{tabularx} % for better tables
14.70 +\usepackage{multirow}
14.71 +\usepackage{listings} % for listings of source code
14.72 +\usepackage{amsmath}
14.73 +
14.74 +
14.75 +\usepackage[austrian,english]{babel} % load babel *before* natbib or jurabib
14.76 +
14.77 +
14.78 +\usepackage[square]{natbib} % natbib but with my own knat.bst
14.79 + % made with the custom-bib package
14.80 +
14.81 +\usepackage{url}
14.82 +\def\UrlFont{\small\ttfamily}
14.83 +
14.84 +\usepackage{latexsym}
14.85 +
14.86 +\usepackage{color}
14.87 +\definecolor{lightgrey}{gray}{0.8}
14.88 +% \definecolor{darkgreen}{rgb}{0,0.2,0}
14.89 +% \definecolor{darkblue}{rgb}{0,0,0.2}
14.90 +% \definecolor{darkred}{rgb}{0.2,0,0}
14.91 +
14.92 +
14.93 +
14.94 +\usepackage{ifpdf}
14.95 +
14.96 +%begin{latexonly}
14.97 +\ifpdf
14.98 + % pdflatex
14.99 + \usepackage[pdftex]{graphicx}
14.100 + \DeclareGraphicsExtensions{.pdf,.jpg,.png}
14.101 + \pdfcompresslevel=9
14.102 + \pdfpageheight=297mm
14.103 + \pdfpagewidth=210mm
14.104 + \usepackage{rotating} % sidewaystable
14.105 + \usepackage[ % hyperref should be last package loaded
14.106 + pdftex,
14.107 + pdftitle={Automating Test Case Generation from Transition Systems via Symbolic Execution and SAT Solving},
14.108 + pdfsubject={Master's Thesis},
14.109 + pdfauthor={Elisabeth Joebstl},
14.110 + pdfkeywords={Model-Based Testing, Conformance Testing, Automated Test Case Generation, Input Output Symbolic Transition Systems, Symbolic Execution, SMT Solving},
14.111 + bookmarks,
14.112 + bookmarksnumbered,
14.113 + linktocpage,
14.114 + pagebackref,
14.115 + colorlinks,
14.116 + linkcolor=black,
14.117 + anchorcolor=black,
14.118 + citecolor=black,
14.119 + urlcolor=black,
14.120 + pdfview={FitH},
14.121 + pdfstartview={Fit},
14.122 + pdfpagemode=UseOutlines, % open bookmarks in Acrobat
14.123 + plainpages=false, % avoids duplicate page number problem
14.124 + pdfpagelabels, % avoids duplicate page number problem
14.125 + ]{hyperref}
14.126 +
14.127 + \renewcommand*{\backref}[1]{}
14.128 + \renewcommand*{\backrefalt}[4]{
14.129 + \ifcase #1
14.130 + (Not cited.)
14.131 + \or
14.132 + (Cited on page~#2.)
14.133 + \else
14.134 + (Cited on pages~#2.)
14.135 + \fi
14.136 + }
14.137 +
14.138 + \renewcommand*{\backrefsep}{, }
14.139 + \renewcommand*{\backreftwosep}{ and~}
14.140 + \renewcommand*{\backreflastsep}{ and~}
14.141 +
14.142 +\else
14.143 + % latex
14.144 + \usepackage{rotating} % sidewaystable
14.145 + \usepackage{graphicx}
14.146 + \DeclareGraphicsExtensions{.eps}
14.147 +\fi
14.148 +%end{latexonly}
14.149 +
14.150 +
14.151 +% \includeonly{intro,biblio} % selective inclusion
14.152 +
14.153 +
14.154 +
14.155 +\newcommand{\halfh}{9.5cm} % height of figures for 2 per page
14.156 +\newcommand{\thirdh}{6cm} % height of figures for 3 per page
14.157 +
14.158 +
14.159 +\setlength{\parskip}{3pt plus 1pt minus 0pt} % vert. space before a paragraph
14.160 +
14.161 +
14.162 +\setcounter{tocdepth}{2} % lowest section level entered in ToC % TODO FIXXME: wieder auf 1 zurücksetzen?
14.163 +\setcounter{secnumdepth}{2} % lowest section level still numbered
14.164 +
14.165 +
14.166 +\input{thesis-macros}
14.167 +
14.168 +
14.169 +% Reduce vertical distance between items
14.170 +% itemize
14.171 +\let\origitemize\itemize
14.172 +\def\itemize{\origitemize\itemsep0pt}
14.173 +%enumerate
14.174 +\let\origenumerate\enumerate
14.175 +\def\enumerate{\origenumerate\itemsep0pt}
14.176 +
14.177 +
14.178 +% FIXXME: bessere Positionierung der Graphiken
14.179 +%\setcounter{totalnumber}{8}
14.180 +%\setcounter{topnumber}{5}
14.181 +%\setcounter{bottomnumber}{5}
14.182 +
14.183 +%\renewcommand{\topfraction}{0.999}
14.184 +%\renewcommand{\bottomfraction}{0.999}
14.185 +%\renewcommand{\textfraction}{0.0005}
14.186 +
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-title.tex Tue Jun 28 17:09:05 2011 +0200
15.3 @@ -0,0 +1,201 @@
15.4 +% --- English Title Page ------------------------------------------------
15.5 +\begin{titlepage}
15.6 +\begin{center}
15.7 +\vspace*{8mm}
15.8 +{\LARGE Bachelor's Thesis}\\
15.9 +
15.10 +\vspace{16mm}
15.11 +
15.12 +{\huge \bf Userinterfaces for Computer Theorem Prover\\
15.13 + feasibility study in the Isac-projekt\\}
15.14 +
15.15 +\vspace{16mm}
15.16 +
15.17 +{\LARGE Marco Steger\textsuperscript{1}}\\
15.18 +
15.19 +\vspace{16mm}
15.20 +
15.21 +{\Large
15.22 +Institute for Software Technology (IST)\\
15.23 +Graz University of Technology\\
15.24 +A-8010 Graz, Austria\\}
15.25 +
15.26 +\vspace{16mm}
15.27 +
15.28 +%TODO TU - figure; Line 26, 76
15.29 +%\begin{figure}[!ht]
15.30 +%\centerline{\includegraphics[width=4cm,keepaspectratio=true]{fig/tug}}
15.31 +%\end{figure}
15.32 +
15.33 +\vspace{16mm}
15.34 +
15.35 +{\large
15.36 +\begin{tabular}{ll}
15.37 +Advisor: & Ass.Prof. Dipl.-Ing. Dr.techn.\ Bernhard Aichernig\\[0.5ex]
15.38 +%TODO Aichernig????
15.39 +Co-Advisor: & Dr.techn.\ Walther Neuper
15.40 +\end{tabular}}
15.41 +
15.42 +\vfill
15.43 +{\large Graz, 30.05.2011????}
15.44 +\vspace{15mm}
15.45 +\end{center}
15.46 +
15.47 +\noindent
15.48 +\underline{\hspace*{3cm}}\\
15.49 +{\footnotesize
15.50 +\textsuperscript{1} E-mail: m.steger@student.tugraz.at\\
15.51 +\copyright ~ Copyright 2011 by the author}
15.52 +
15.53 +
15.54 +
15.55 +% --- German Title Page -------------------------------------------------
15.56 +\selectlanguage{austrian}
15.57 +
15.58 +\newpage
15.59 +\begin{center}
15.60 +\vspace*{8mm}
15.61 +{\LARGE Bachelorarbeit}\\
15.62 +
15.63 +\vspace{16mm}
15.64 +
15.65 +{\huge \bf Userinterfaces f\"ur Computer Theorem Prover\\
15.66 + Machbarkeits-Studie im Isac-Projekt\\}
15.67 +
15.68 +\vspace{16mm}
15.69 +
15.70 +{\LARGE Marco Steger\textsuperscript{1}}\\
15.71 +
15.72 +\vspace{16mm}
15.73 +
15.74 +{\Large
15.75 +Institut f\"ur Softwaretechnologie (IST)\\
15.76 +Technische Universit\"at Graz\\
15.77 +A-8010 Graz\\}
15.78 +
15.79 +\vspace{16mm}
15.80 +
15.81 +%\begin{figure}[!ht]
15.82 +%\centerline{\includegraphics[width=4cm,keepaspectratio=true]{fig/tug}}
15.83 +%\end{figure}
15.84 +
15.85 +\vspace{16mm}
15.86 +
15.87 +%TODO Aichernig????
15.88 +{\large
15.89 +\begin{tabular}{ll}
15.90 +Gutachter: & Ass.Prof. Dipl.-Ing. Dr.techn.\ Bernhard Aichernig\\[0.5ex]
15.91 +Mitbetreuer: & Dr.techn.\ Walther Neuper
15.92 +\end{tabular}}
15.93 +
15.94 +\vspace{16mm}
15.95 +{\large Graz, 30.05.2011}
15.96 +
15.97 +\vfill
15.98 +Diese Arbeit ist in deutscher Sprache verfasst.
15.99 +\end{center}
15.100 +
15.101 +\noindent
15.102 +\underline{\hspace*{3cm}}\\
15.103 +{\footnotesize
15.104 +\textsuperscript{1} E-Mail: m.steger@student.tugraz.at\\
15.105 +\copyright ~ Copyright 2011, Marco Steger}
15.106 +\end{titlepage}
15.107 +
15.108 +\selectlanguage{english}
15.109 +
15.110 +
15.111 +% --- English Abstract --------------------------------------------------
15.112 +\pagestyle{plain}
15.113 +\pagenumbering{roman}
15.114 +\newpage
15.115 +
15.116 +\vspace*{25mm}
15.117 +
15.118 +\begin{changemargin}{15mm}{15mm}
15.119 +\begin{center}
15.120 +{\Large\bfseries Abstract}
15.121 +\end{center}
15.122 +\vspace*{7mm}
15.123 +
15.124 +Place english abstract here.
15.125 +
15.126 +\vspace{5mm}
15.127 +\noindent
15.128 +{\large\bfseries Keywords:}
15.129 +some english keywords
15.130 +
15.131 +
15.132 +
15.133 +% --- German Abstract ---------------------------------------------------
15.134 +\selectlanguage{austrian}
15.135 +\newpage
15.136 +
15.137 +\vspace*{10mm}
15.138 +
15.139 +\begin{center}
15.140 +{\Large\bfseries Kurzfassung}
15.141 +\end{center}
15.142 +\vspace*{2mm}
15.143 +
15.144 +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.
15.145 +
15.146 +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.
15.147 +
15.148 +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.
15.149 +
15.150 +\vspace{5mm}
15.151 +\noindent
15.152 +{\large\bfseries Schlagworte:}
15.153 +einige deutsche Schlagworte
15.154 +
15.155 +\selectlanguage{english}
15.156 +\end{changemargin}
15.157 +
15.158 +
15.159 +% --- Pledge ------------------------------------------------------------
15.160 +\newpage
15.161 +\vspace*{20mm}
15.162 +
15.163 +\begin{center}
15.164 +{\Large\bfseries Statutory Declaration}
15.165 +\end{center}
15.166 +\vspace{5mm}
15.167 +\noindent
15.168 +I declare that I have authored this thesis independently, that I have not used other than the declared
15.169 +sources/resources, and that I have explicitly marked all material which has been quoted either
15.170 +literally or by content from the used sources.
15.171 +
15.172 +\vspace{2cm}
15.173 +
15.174 +\noindent
15.175 +\begin{tabular}{ccc}
15.176 +\hspace*{6cm} & \hspace*{2cm} & \hspace*{6.7cm}\\
15.177 +\dotfill & & \dotfill\\
15.178 +place, date & & (signature)\\
15.179 +\end{tabular}
15.180 +
15.181 +\vspace{35mm}
15.182 +
15.183 +
15.184 +\selectlanguage{austrian}
15.185 +
15.186 +\begin{center}
15.187 +{\Large\bfseries Eidesstattliche Erkl\"arung}
15.188 +\end{center}
15.189 +\vspace{5mm}
15.190 +\noindent
15.191 +Ich erkl\"are an Eides statt, dass ich die vorliegende Arbeit selbstst\"andig verfasst, andere als die
15.192 +angegebenen Quellen/Hilfsmittel nicht benutzt, und die den benutzten Quellen w\"ortlich und inhaltlich
15.193 +entnommenen Stellen als solche kenntlich gemacht habe.
15.194 +
15.195 +\vspace{2cm}
15.196 +
15.197 +\noindent
15.198 +\begin{tabular}{ccc}
15.199 +\hspace*{6cm} & \hspace*{2cm} & \hspace*{6.7cm}\\
15.200 +\dotfill & & \dotfill\\
15.201 +Ort, Datum & & (Unterschrift)\\
15.202 +\end{tabular}
15.203 +
15.204 +\selectlanguage{english}
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis.tex Tue Jun 28 17:09:05 2011 +0200
16.3 @@ -0,0 +1,70 @@
16.4 +\documentclass[11pt]{report}
16.5 +%\usepackage{ngerman}
16.6 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
16.7 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
16.8 +
16.9 +\include{thesis-preamble}
16.10 +
16.11 +\begin{document}
16.12 +
16.13 +\lstset{ % set parameters for listings
16.14 + language=,
16.15 + basicstyle=\small,
16.16 + tabsize=2,
16.17 + xleftmargin=2mm,
16.18 + xrightmargin=2mm,
16.19 + float=htb,
16.20 + frame=shadowbox,
16.21 + framexleftmargin=2mm,
16.22 + rulesepcolor=\color{lightgrey},
16.23 + numbers=left,
16.24 + numberstyle=\scriptsize,
16.25 + extendedchars,
16.26 + breaklines,
16.27 + showtabs=false,
16.28 + showspaces=false,
16.29 + showstringspaces=false,
16.30 + keywordstyle=\bfseries,
16.31 + identifierstyle=\ttfamily,
16.32 + stringstyle=,
16.33 + captionpos=b,
16.34 + abovecaptionskip=\abovecaptionskip,
16.35 + belowcaptionskip=\belowcaptionskip,
16.36 + aboveskip=\floatsep,
16.37 +}
16.38 +
16.39 +
16.40 +%\frontmatter
16.41 +\normalsize
16.42 +\pagestyle{empty} % for title pages
16.43 +
16.44 +\pagenumbering{alph}
16.45 +\include{thesis-title} % Title Pages, Abstracts, Pledge
16.46 +\include{thesis-acknowl} % Acknowledgements
16.47 +\include{thesis-contents} % Table of Contents, List of Figures, List of Tables
16.48 +
16.49 +
16.50 +%\mainmatter
16.51 +\pagestyle{fancy} % for main pages
16.52 +\pagenumbering{arabic} % for main pages
16.53 +
16.54 +\include{thesis-intro} % Introduction
16.55 +\include{content}
16.56 +% \include{your main files}
16.57 +
16.58 +%\include{thesis-conclusion} % Conclusion and Future Work
16.59 +
16.60 +
16.61 +\appendix
16.62 +% \noappendicestocpagenum
16.63 +% \addappheadtotoc
16.64 +
16.65 +\include{thesis-appendix} % Appendix A
16.66 +
16.67 +
16.68 +%\backmatter
16.69 +\include{thesis-biblio} % Bibliography
16.70 +% \include{glossary} % Glossary
16.71 +% \include{index} % Index
16.72 +
16.73 +\end{document}
16.74 \ No newline at end of file
17.1 --- a/doc-src/isac/msteger/official_docu/master_thesis.bib Tue Jun 28 16:25:19 2011 +0200
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,162 +0,0 @@
17.4 -% Add your bibtex entries
17.5 -@inproceedings{Aspinall:2007:FIP:1420412.1420429,
17.6 - author = {Aspinall, David and L\"{u}th, Christoph and Winterstein, Daniel},
17.7 - title = {A Framework for Interactive Proof},
17.8 - booktitle = {Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference},
17.9 - series = {Calculemus '07 / MKM '07},
17.10 - year = {2007},
17.11 - isbn = {978-3-540-73083-5},
17.12 - location = {Hagenberg, Austria},
17.13 - pages = {161--175},
17.14 - numpages = {15},
17.15 - url = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
17.16 - doi = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
17.17 - acmid = {1420429},
17.18 - publisher = {Springer-Verlag},
17.19 - address = {Berlin, Heidelberg},
17.20 -}
17.21 -
17.22 -@Book{armstrong:erlang96,
17.23 - author = {Armstrong, Joe and others},
17.24 - title = {Concurrent Programming in Erlang},
17.25 - publisher = {Prentice Hall},
17.26 - year = {1996}
17.27 -}
17.28 -
17.29 -@TechReport{odersky:scala06,
17.30 - author = {Odersky, Martin and others},
17.31 - title = {An Overview of the Scala Programming Language},
17.32 - institution = {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)},
17.33 - year = {2006},
17.34 - type = {Technical Report LAMP-REPORT-2006-001},
17.35 - address = {1015 Lausanne, Switzerland},
17.36 - note = {Second Edition},
17.37 - annote = {http://www.scala-lang.org/sites/default/files/linuxsoft_archives/docu/files/ScalaOverview.pdf}
17.38 -}
17.39 -
17.40 -@article{Haller:2009:SAU:1496391.1496422,
17.41 - author = {Haller, Philipp and Odersky, Martin},
17.42 - title = {Scala Actors: Unifying thread-based and event-based programming},
17.43 - journal = {Theor. Comput. Sci.},
17.44 - volume = {410},
17.45 - issue = {2-3},
17.46 - month = {February},
17.47 - year = {2009},
17.48 - issn = {0304-3975},
17.49 - pages = {202--220},
17.50 - numpages = {19},
17.51 - url = {http://portal.acm.org/citation.cfm?id=1496391.1496422},
17.52 - doi = {10.1016/j.tcs.2008.09.019},
17.53 - acmid = {1496422},
17.54 - publisher = {Elsevier Science Publishers Ltd.},
17.55 - address = {Essex, UK},
17.56 - keywords = {Actors, Concurrent programming, Events, Threads},
17.57 -}
17.58 -
17.59 -@InProceedings{scala:jmlc06,
17.60 - author = {Philipp Haller and Martin Odersky},
17.61 - title = {Event-Based Programming without Inversion of Control},
17.62 - booktitle = {Proc. Joint Modular Languages Conference},
17.63 - year = 2006,
17.64 - series = {Springer LNCS}
17.65 -}
17.66 -
17.67 -
17.68 -@InProceedings{makarius:isa-scala-jedit,
17.69 - author = {Makarius Wenzel},
17.70 - title = {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
17.71 - booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
17.72 - year = {2010},
17.73 - editor = {C. Sacerdoti Coen and D. Aspinall},
17.74 - address = {Edinburgh, Scotland},
17.75 - month = {July},
17.76 - organization = {FLOC 2010 Satellite Workshop},
17.77 - note = {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
17.78 -}
17.79 -
17.80 -@Book{db:dom-eng,
17.81 - author = {Bj{\o}rner, Dines},
17.82 - title = {Domain Engineering. Technology Management, Research and Engineering},
17.83 - publisher = {JAIST Press},
17.84 - year = {2009},
17.85 - month = {Feb},
17.86 - series = {COE Research Monograph Series},
17.87 - volume = {4},
17.88 - address = {Nomi, Japan}
17.89 -}
17.90 -
17.91 -@inproceedings{Haftmann-Nipkow:2010:code,
17.92 - author = {Florian Haftmann and Tobias Nipkow},
17.93 - title = {Code Generation via Higher-Order Rewrite Systems},
17.94 - booktitle = {Functional and Logic Programming, 10th International
17.95 -Symposium: {FLOPS} 2010},
17.96 - year = {2010},
17.97 - publisher = {Springer},
17.98 - series = {Lecture Notes in Computer Science},
17.99 - volume = {6009}
17.100 -}
17.101 -
17.102 -@Manual{coq1999,
17.103 - title = {The Coq Proof Assistant},
17.104 - author = {Barras, B. and others},
17.105 - organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},
17.106 - month = {July},
17.107 - year = {1999},
17.108 - pnote={},status={cited},source={mkm01.caprotti},location={}
17.109 -}
17.110 -
17.111 -@Book{meta-ML,
17.112 - author = {Gordon,M. and Milner,R. and Wadsworth,C. P.},
17.113 - title = {Edinburgh LCF: A Mechanised Logic of Computation},
17.114 - publisher = { Springer-Verlag},
17.115 - year = {1979},
17.116 - volume = {78},
17.117 - series = {Lecture Notes in Computer Science}
17.118 -}
17.119 -
17.120 -@book{Paulson:Isa94,
17.121 - title={Isabelle: a generic theorem prover},
17.122 - author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994},
17.123 - volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={},
17.124 - note={With contributions by Topias Nipkow},
17.125 - status={},source={},location={-}
17.126 - }
17.127 -
17.128 -@Book{pl:milner97,
17.129 - author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
17.130 - title = {The Definition of Standard ML (Revised)},
17.131 - publisher = {The MIT Press},
17.132 - year = 1997,
17.133 - address = {Cambridge, London},
17.134 - annote = {97bok375}
17.135 -}
17.136 -
17.137 -@Article{back-grundy-wright-98,
17.138 - author = {Back, Ralph and Grundy, Jim and von Wright, Joakim},
17.139 - title = {Structured Calculational Proof},
17.140 - journal = {Formal Aspects of Computing},
17.141 - year = {1998},
17.142 - number = {9},
17.143 - pages = {469-483}
17.144 -}
17.145 -
17.146 -@Manual{isar-impl,
17.147 - title = {The {Isabelle/Isar} Implementation},
17.148 - author = {Makarius Wenzel},
17.149 - month = {April 19},
17.150 - year = {2009},
17.151 - note = {With contributions by Florian Haftmann and Larry Paulson}
17.152 -}
17.153 -
17.154 -@InProceedings{wenzel:isar,
17.155 - author = {Wenzel, Markus},
17.156 - title = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
17.157 - booktitle = {Theorem Proving in Higher Order Logics},
17.158 - year = {1999},
17.159 - editor = {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
17.160 - series = {LNCS 1690},
17.161 - organization = {12th International Conference TPHOLs'99},
17.162 - publisher = {Springer}
17.163 -}
17.164 -
17.165 -
18.1 --- a/doc-src/isac/msteger/official_docu/thesis-acknowl.tex Tue Jun 28 16:25:19 2011 +0200
18.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
18.3 @@ -1,45 +0,0 @@
18.4 -%\begin{changemargin}{1.5cm}{1.5cm}
18.5 -
18.6 -%\chapter*{Acknowledgements}
18.7 -%\addcontentsline{toc}{chapter}{Acknowledgements}
18.8 -
18.9 -
18.10 -
18.11 -\begin{center}
18.12 -{\Large\bfseries Acknowledgements}
18.13 -\end{center}
18.14 -%\vspace*{3mm}
18.15 -
18.16 -\begin{changemargin}{1.5cm}{1.5cm}
18.17 -I would like to thank ...
18.18 -
18.19 -\begin{flushright}
18.20 -your name \\ {\small place, county, date}
18.21 -\end{flushright}
18.22 -\end{changemargin}
18.23 -
18.24 -\selectlanguage{austrian}
18.25 -
18.26 -\vspace*{5mm}
18.27 -
18.28 -\begin{center}
18.29 -{\Large\bfseries Danksagung}
18.30 -\end{center}
18.31 -%\vspace*{0mm}
18.32 -
18.33 -\begin{changemargin}{1.5cm}{1.5cm}
18.34 -Ich möchte mich herzlich bei allen bedanken, die ...
18.35 -
18.36 -\begin{flushright}
18.37 -Dein Name \\ {\small Ort, Land, Datum}
18.38 -\end{flushright}
18.39 -\end{changemargin}
18.40 -
18.41 -\selectlanguage{english}
18.42 -
18.43 -
18.44 -
18.45 -
18.46 -
18.47 -
18.48 -
19.1 --- a/doc-src/isac/msteger/official_docu/thesis-appendix.tex Tue Jun 28 16:25:19 2011 +0200
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,339 +0,0 @@
19.4 -\chapter{Milestones und Arbeitsprotokolle}\label{milestones} %\ref doesnt work outside this file ?!?
19.5 -\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010}
19.6 -\begin{itemize}
19.7 -\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010
19.8 -\item Charakteristika der Programmsprache Scala: beendet am 27.09.2010
19.9 -\item Scala Actors: beendet am 12.08.2010
19.10 -\end{itemize}
19.11 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
19.12 -\hline
19.13 -Datum & T\"atigkeit & Einheiten \\ \hline
19.14 -12.07.2010 & Meeting: erste Besprechung und Erkl\"{a}rungen zu Isabelle, Isac und CTPs & 2 \\ \hline
19.15 -15.07.2010 & Recherche \"{u}ber Isabelle und CTPs & 3 \\ \hline
19.16 -20.07.2010 & Meeting: Besprechen der grunds\"{a}tzlichen Vorgangsweise und Ziele & 1 \\ \hline
19.17 -23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenh\"{a}nge mit Isac abkl\"{a}ren & 1 \\ \hline
19.18 -30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise \"{u}ber Backs 'structured derivations'; Begriffserkl\"{a}rung & 3 \\ \hline
19.19 -01.08.2010 & Recherche: Buch f\"{u}r Scala & 2 \\ \hline
19.20 -03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
19.21 -05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
19.22 -06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
19.23 -08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
19.24 -09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
19.25 -12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
19.26 -24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
19.27 -25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
19.28 -27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline \hline
19.29 - & Anzahl der Einheiten & 44 \\
19.30 -\hline
19.31 -\end{tabular}
19.32 -
19.33 -
19.34 -\section{Technische Voraussetzungen hergestellt: beendet am 02.08.2010}
19.35 -\begin{itemize}
19.36 -\item Isabelle installiert, Filestruktur bekannt: beendet am 02.08.2010
19.37 -\item Scala in NetBeans eingebunden: beendet am 22.07.2010
19.38 -\item Mercurial installiert und einrichten des Repositories: beendet am 19.07.2010
19.39 -\end{itemize}
19.40 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
19.41 -\hline
19.42 -Datum & T\"atigkeit & Einheiten \\ \hline
19.43 -19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
19.44 -20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
19.45 -21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
19.46 -22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
19.47 -23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausf\"{u}hren: testen & 5 \\ \hline
19.48 -27.07.2010 & Isabelle-jEdit-Plugin: \"{a}nderungen an der Projektstruktur & 7 \\ \hline
19.49 -28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
19.50 -29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
19.51 -30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung \"{u}ber Erfahrungen mit Filestruktur & 4 \\ \hline
19.52 -02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
19.53 - & Anzahl der Einheiten & 60 \\
19.54 -\hline
19.55 -\end{tabular}
19.56 -
19.57 -\section{NetBeans-Projekt aufgesetzt: beendet am 02.08.2010}
19.58 -\begin{itemize}
19.59 -\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: beendet am 02.08.2010
19.60 -\item jEdit-Plugin: XML-Files f\"{u}r ISAC vorbereitet: beendet am 22.07.2010
19.61 -\item jEdit-Plugin: Source files geschrieben: beendet am 19.07.2010
19.62 -\end{itemize}
19.63 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
19.64 -\hline
19.65 -Datum & T\"atigkeit & Einheiten \\ \hline
19.66 -10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
19.67 -11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
19.68 -21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
19.69 -22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten f\"{u}r ISAC & 3 \\ \hline
19.70 -24.08.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 6 \\ \hline
19.71 -26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach L\"{o}sungen & 3 \\ \hline
19.72 -28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
19.73 -29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
19.74 -30.08.2010 & Isabelle-jEdit-Plugin endlich vollst\"{a}ndig lauff\"{a}hig gebracht & 4 \\ \hline
19.75 -01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
19.76 -04.09.2010 & Umarbeiten des Isabelle-Plugins f\"{u}r ISAC & 5 \\ \hline
19.77 -20.09.2010 & Einrichten des Laptops f\"{u}r Isabelle-Isac & 4 \\ \hline
19.78 -22.09.2010 & Meeting: Fortschrittsbericht, kurze Einf\"{u}hrung f\"{u}r Mitstreiter & 3 \\ \hline
19.79 -
19.80 -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
19.81 -30.09.2010 & QN: Start mit \"{u}bersetzten der Sourcefiles & 5 \\ \hline
19.82 -02.10.2010 & QN: \"{U}bersetzten der Sourcefiles & 6 \\ \hline
19.83 -04.10.2010 & QN: \"{U}bersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
19.84 -05.10.2010 & QN: QN vollst\"andig in Scala \"{u}bersetzt, testen & 2 \\ \hline \hline
19.85 - & Anzahl der Einheiten & 71 \\
19.86 -\hline
19.87 -\end{tabular}
19.88 -
19.89 -\section{Experimentelle Parser implementiert: beendet am 04.03.2011}
19.90 -\begin{itemize}
19.91 -\item Experimente mit dem SideKick-Parser abgeschlossen: beendet am 03.02.2011
19.92 -\item Verbindung zu Isabelle-Pure hergestellt: beendet am 04.03.2011
19.93 -\item Implementierung des Scala-Parsers: aufgeschoben
19.94 -\end{itemize}
19.95 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
19.96 -\hline
19.97 -Datum & T\"atigkeit & Einheiten \\ \hline
19.98 -28.01.2011 & Testen des SideKick-Parsers im Isabelle-Plugin & 2 \\ \hline
19.99 -29.01.2011 & Leichte Modifikationen des SideKick-Parsers im Isabelle-Plugin & 1 \\ \hline
19.100 -08.02.2011 & Besprechung zum Abschluss der praktischen Arbeiten & 1 \\ \hline
19.101 -16.02.2011 & Erstellen des Isabelle-Pur jar-Files & 1 \\ \hline
19.102 -19.02.2011 & Behebung des Problems mit den Umgebungsvariablen & 1 \\ \hline
19.103 -03.03.2011 & Erzeugung des Pure.jar Package m\"{o}glich & 2 \\ \hline
19.104 -04.04.2011 & Verbindung zwischen Plugin und Isabelle-Pure hergestellt und getestet & 3 \\ \hline
19.105 -08.04.2011 & Besprechung: Implementierung des experimentellen Parsers wird nicht mehr durchgef\"{u}hrt & 1 \\ \hline \hline
19.106 - & Anzahl der Einheiten & 12 \\
19.107 -\hline
19.108 -\end{tabular}
19.109 -
19.110 -\section{Verfassen der Dokumentation und abschliesende Arbeiten: beendet am TO.DO.2011}
19.111 -\begin{itemize}
19.112 -\item Bacc.-Protokoll fertiggestellt: beendet am 01.03.2011
19.113 -\item Dokumentation: erste Version fertiggestellt: beendet am 28.04.2011
19.114 -\item Dokumentation abgeschlossen: beendet am TO.DO.2011
19.115 -\end{itemize}
19.116 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
19.117 -\hline
19.118 -Datum & T\"atigkeit & Einheiten \\ \hline
19.119 -01.03.2011 & Besprechung zum Ablauf der Dokumentationsarbeiten: Protokoll und Dokumentation & 1 \\ \hline
19.120 -01.03.2011 & Erstellen des Protokolls & 2 \\ \hline
19.121 -08.03.2011 & Besprechung zur Doku und zur Schnittstelle zu Isabelle-Pure & 1 \\ \hline
19.122 -17.03.2011 & Dokumentation schreiben & 2 \\ \hline
19.123 -19.03.2011 & Dokumentation schreiben & 3 \\ \hline
19.124 -24.04.2011 & Dokumentation schreiben & 2 \\ \hline
19.125 -25.04.2011 & Dokumentation schreiben & 4 \\ \hline
19.126 -27.04.2011 & Dokumentation schreiben & 2 \\ \hline
19.127 -28.04.2011 & Dokumentation: Fertigstellen der ersten Version & 3 \\ \hline \hline
19.128 - & Anzahl der Einheiten & 20 \\
19.129 -\hline
19.130 -\end{tabular}
19.131 -
19.132 -\section{Pr\"asentation der Arbeit im IST-Seminar: beendet am 21.06.2011}
19.133 -\begin{itemize}
19.134 -\item Pr\"asentation fertiggestellt: beendet am 19.06.2011
19.135 -\item Pr\"asentation: abgehalten am 21.06.2011
19.136 -\end{itemize}
19.137 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
19.138 -\hline
19.139 -Datum & T\"atigkeit & Einheiten \\ \hline
19.140 -06.06.2011 & Planung der Pr\"asentation & 2 \\ \hline
19.141 -16.06.2011 & Verfassen der Pr\"asentation & 2 \\ \hline
19.142 -18.06.2011 & Verfassen der Pr\"asentation & 3 \\ \hline
19.143 -19.06.2011 & Pr\"asentation: Feinschliff & 2 \\ \hline
19.144 -20.06.2011 & Vorbereiten der Pr\"asentation& 3 \\ \hline
19.145 -21.06.2011 & Abhaltung und nachfolgende Diskussion & 1 \\ \hline \hline
19.146 - & Anzahl der Einheiten & 13 \\
19.147 - \hline
19.148 -\end{tabular}
19.149 -
19.150 -\chapter{Filestruktur Isabelle}
19.151 -\section{jar-Packete}
19.152 -\textbf{----- for "isabelle jedit \&"; contained in Isabelle\_bundle} \\
19.153 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar \\
19.154 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar \\
19.155 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar \\
19.156 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar \\
19.157 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \\
19.158 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar \\
19.159 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar \\
19.160 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar \\
19.161 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar \\
19.162 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar \\
19.163 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar \\
19.164 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar \\
19.165 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar \\
19.166 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar \\
19.167 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar \\
19.168 -\textbf{----- scala system; contained in Isabelle\_bundle} \\
19.169 -./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar \\
19.170 -./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar \\
19.171 -./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar \\
19.172 -./contrib/scala-2.8.1.final/lib/scala-compiler.jar \\
19.173 -./contrib/scala-2.8.1.final/lib/scalap.jar \\
19.174 -./contrib/scala-2.8.1.final/lib/scala-swing.jar \\
19.175 -./contrib/scala-2.8.1.final/lib/scala-library.jar \\
19.176 -./contrib/scala-2.8.1.final/lib/jline.jar \\
19.177 -./contrib/scala-2.8.1.final/lib/scala-dbc.jar \\
19.178 -./contrib/scala-2.8.1.final/src/scala-library-src.jar \\
19.179 -./contrib/scala-2.8.1.final/src/scala-swing-src.jar \\
19.180 -./contrib/scala-2.8.1.final/src/scala-compiler-src.jar \\
19.181 -./contrib/scala-2.8.1.final/src/scala-dbc-src.jar \\
19.182 -./contrib/scala-2.8.1.final/src/sbaz-src.jar \\
19.183 -\textbf{----- Isars entry to SML from Scala-layer; } \\
19.184 -\textit{created according to 4.3.\#3 }\\
19.185 -./lib/classes/isabelle-scala.jar \\
19.186 -./lib/classes/Pure.jar \\\\
19.187 -\textit{\textbf{===== all below for NetBeans}} \\\\
19.188 -\textbf{----- standard Isabelle, started by $<RUN>$ in NetBeans} \\
19.189 - \textit{description in 2.2.2} \\
19.190 -./src/Tools/jEdit/dist/jars/jedit.jar \\
19.191 -./src/Tools/jEdit/dist/jars/SideKick.jar \\
19.192 -./src/Tools/jEdit/dist/jars/Console.jar \\
19.193 -./src/Tools/jEdit/dist/jars/Pure.jar \\
19.194 -./src/Tools/jEdit/dist/jars/scala-compiler.jar \\
19.195 -./src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar \\
19.196 -./src/Tools/jEdit/dist/jars/cobra.jar \\
19.197 -./src/Tools/jEdit/dist/jars/js.jar \\
19.198 -./src/Tools/jEdit/dist/jars/Hyperlinks.jar \\
19.199 -./src/Tools/jEdit/dist/jars/scala-swing.jar \\
19.200 -./src/Tools/jEdit/dist/jars/scala-library.jar \\
19.201 -./src/Tools/jEdit/dist/jars/ErrorList.jar \\
19.202 -\textbf{----- source of jEdit, required for $<DEBUG>$ in NetBeans; \\}
19.203 - adapted from NetBeans' webpages, \\
19.204 - \textit{description in 2.2.3.\#5} \\
19.205 -./src/Tools/jEditC/contrib/jEdit/build/jars/SideKick.jar \\
19.206 -./src/Tools/jEditC/contrib/jEdit/build/jars/Console.jar \\
19.207 -./src/Tools/jEditC/contrib/jEdit/build/jars/Pure.jar \\
19.208 -./src/Tools/jEditC/contrib/jEdit/build/jars/Isac.jar \\
19.209 -./src/Tools/jEditC/contrib/jEdit/build/jars/QuickNPScala.jar \\
19.210 -./src/Tools/jEditC/contrib/jEdit/build/jars/scala-compiler.jar \\
19.211 -./src/Tools/jEditC/contrib/jEdit/build/jars/Isabelle-jEdit.jar \\
19.212 -./src/Tools/jEditC/contrib/jEdit/build/jars/cobra.jar \\
19.213 -./src/Tools/jEditC/contrib/jEdit/build/jars/js.jar \\
19.214 -./src/Tools/jEditC/contrib/jEdit/build/jars/Hyperlinks.jar \\
19.215 -./src/Tools/jEditC/contrib/jEdit/build/jars/scala-swing.jar \\
19.216 -./src/Tools/jEditC/contrib/jEdit/build/jars/scala-library.jar \\
19.217 -./src/Tools/jEditC/contrib/jEdit/build/jars/ErrorList.jar \\
19.218 -./src/Tools/jEditC/contrib/jEdit/build/jEdit.jar \\
19.219 -\textbf{----- demo plugin, started by $<RUN>$ in NetBeans \\}
19.220 - \textit{description in 2.2.3.\#4} \\
19.221 -./src/Tools/jEditC/dist/jars/SideKick.jar \\
19.222 -./src/Tools/jEditC/dist/jars/Console.jar \\
19.223 -./src/Tools/jEditC/dist/jars/Pure.jar \\
19.224 -./src/Tools/jEditC/dist/jars/Isac.jar \\
19.225 -./src/Tools/jEditC/dist/jars/scala-compiler.jar \\
19.226 -./src/Tools/jEditC/dist/jars/cobra.jar \\
19.227 -./src/Tools/jEditC/dist/jars/js.jar \\
19.228 -./src/Tools/jEditC/dist/jars/Hyperlinks.jar \\
19.229 -./src/Tools/jEditC/dist/jars/scala-swing.jar \\
19.230 -./src/Tools/jEditC/dist/jars/scala-library.jar \\
19.231 -./src/Tools/jEditC/dist/jars/ErrorList.jar \\
19.232 -
19.233 -\section{Scala-Files: Isabelle-Pure}
19.234 -\textbf{General:}\\
19.235 -./src/Pure/General/xml.scala\\
19.236 -./src/Pure/General/linear\_set.scala\\
19.237 -./src/Pure/General/symbol.scala\\
19.238 -./src/Pure/General/exn.scala\\
19.239 -./src/Pure/General/position.scala\\
19.240 -./src/Pure/General/scan.scala\\
19.241 -./src/Pure/General/xml\_data.scala\\
19.242 -./src/Pure/General/yxml.scala\\
19.243 -./src/Pure/General/markup.scala\\
19.244 -./src/Pure/General/sha1.scala\\
19.245 -./src/Pure/General/timing.scala\\
19.246 -./src/Pure/General/pretty.scala\\
19.247 -\textbf{Concurent:}\\
19.248 -./src/Pure/Concurrent/volatile.scala\\
19.249 -./src/Pure/Concurrent/future.scala\\
19.250 -./src/Pure/Concurrent/simple\_thread.scala\\
19.251 -\textbf{Thy:}\\
19.252 -./src/Pure/Thy/html.scala\\
19.253 -./src/Pure/Thy/completion.scala\\
19.254 -./src/Pure/Thy/thy\_header.scala\\
19.255 -./src/Pure/Thy/thy\_syntax.scala\\
19.256 -./src/Pure/Isac/isac.scala\\
19.257 -./src/Pure/library.scala\\
19.258 -\textbf{Isar:}\\
19.259 -./src/Pure/Isar/keyword.scala\\
19.260 -./src/Pure/Isar/outer\_syntax.scala\\
19.261 -./src/Pure/Isar/token.scala\\
19.262 -./src/Pure/Isar/parse.scala\\
19.263 -\textbf{Isac:}\\
19.264 -\textit{./src/Pure/Isac/isac.scala}\\
19.265 -\textbf{System:}\\
19.266 -./src/Pure/System/gui\_setup.scala\\
19.267 -./src/Pure/System/isabelle\_system.scala\\
19.268 -./src/Pure/System/swing\_thread.scala\\
19.269 -./src/Pure/System/download.scala\\
19.270 -./src/Pure/System/session\_manager.scala\\
19.271 -./src/Pure/System/standard\_system.scala\\
19.272 -./src/Pure/System/isabelle\_syntax.scala\\
19.273 -./src/Pure/System/session.scala\\
19.274 -./src/Pure/System/platform.scala\\
19.275 -./src/Pure/System/cygwin.scala\\
19.276 -./src/Pure/System/event\_bus.scala\\
19.277 -./src/Pure/System/isabelle\_process.scala\\
19.278 -\textbf{PIDE}\\
19.279 -./src/Pure/PIDE/document.scala\\
19.280 -./src/Pure/PIDE/markup\_tree.scala\\
19.281 -./src/Pure/PIDE/text.scala\\
19.282 -./src/Pure/PIDE/command.scala\\
19.283 -./src/Pure/PIDE/isar\_document.scala \\
19.284 -
19.285 -
19.286 -\chapter{Das Skript \textit{isac\_jedit}}
19.287 -
19.288 -\textit{
19.289 -\#$!$/usr/bin/env bash
19.290 -cd src/Pure/ \\
19.291 -echo "Building Pure.jar" \\
19.292 -../../bin/isabelle env ./build-jars \\
19.293 -echo "copying Pure.jar to contrib/jedit" \\
19.294 -cp ../../lib/classes/Pure.jar ../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ \\
19.295 -echo "Building Isac.jar" \\
19.296 -cd /home/gadei/isac/isa/src/Tools/jEditC \\
19.297 -ant jar \\
19.298 -cd /home/gadei/isac/isa/src/Pure/ \\
19.299 -echo "copying Isac.jar to contrib/jedit" \\
19.300 -cp ../Tools/jEditC/contrib/jEdit/build/jars/Isac.jar ../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ \\
19.301 -echo "Done!" \\
19.302 -}
19.303 -
19.304 -\chapter{Filestruktur f\"ur die Entwicklung des SD-Plugins}
19.305 -
19.306 -build.xml\\
19.307 -makedist\\
19.308 -manifest.mf\\
19.309 -README\_BUILD\\
19.310 -\textbf{build/*}\\
19.311 -\textbf{contrib/*}\\
19.312 -\textbf{dist/*}\\
19.313 -\textbf{plugin/}build.xml\\
19.314 -\textbf{plugin/}changes40.txt\\
19.315 -\textbf{plugin/}changes42.txt\\
19.316 -\textbf{plugin/}description.html\\
19.317 -\textbf{plugin/}IsacActions.java\\
19.318 -\textbf{plugin/}Isac.iml\\
19.319 -\textbf{plugin/}Isac.java\\
19.320 -\textbf{plugin/}IsacOptionPane.java\\
19.321 -\textbf{plugin/}IsacPlugin.java\\
19.322 -\textbf{plugin/}IsacTextArea.java\\
19.323 -\textbf{plugin/}IsacToolPanel.java\\
19.324 -\textbf{plugin/}plugin\\
19.325 -\textbf{plugin/}README.txt\\
19.326 -\textbf{nbproject/*}\\
19.327 -\textbf{src/}actions.xml\\
19.328 -\textbf{src/}changes40.txt\\
19.329 -\textbf{src/}changes42.txt\\
19.330 -\textbf{src/}description.html\\
19.331 -\textbf{src/}dockables.xml\\
19.332 -\textit{\textbf{src/}IsacActions.scala\\}
19.333 -\textbf{src/}Isac.iml\\
19.334 -\textit{\textbf{src/}IsacOptionPane.scala\\}
19.335 -\textit{\textbf{src/}IsacPlugin.scala\\}
19.336 -\textbf{src/}Isac.props\\
19.337 -\textit{\textbf{src/}Isac.scala\\}
19.338 -\textit{\textbf{src/}IsacTextArea.scala\\}
19.339 -\textit{\textbf{src/}IsacToolPanel.scala\\}
19.340 -\textbf{src/}manifest.mf\\
19.341 -\textbf{src/}README.txt\\
19.342 -\textbf{src/}users-guide.xml \\
19.343 \ No newline at end of file
20.1 --- a/doc-src/isac/msteger/official_docu/thesis-biblio.tex Tue Jun 28 16:25:19 2011 +0200
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,15 +0,0 @@
20.4 -{
20.5 -
20.6 -\bibliographystyle{plain}
20.7 -
20.8 -
20.9 -% the names of the bib files used
20.10 -
20.11 -\phantomsection
20.12 -\addcontentsline{toc}{chapter}{Bibliography}
20.13 -\bibliography{master_thesis.bib}
20.14 -%\bibliography{../master_thesis.bib}
20.15 -
20.16 -}
20.17 -
20.18 -
21.1 --- a/doc-src/isac/msteger/official_docu/thesis-conclusion.tex Tue Jun 28 16:25:19 2011 +0200
21.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
21.3 @@ -1,2 +0,0 @@
21.4 -\chapter{Concluding Remarks}
21.5 -...
21.6 \ No newline at end of file
22.1 --- a/doc-src/isac/msteger/official_docu/thesis-contents.tex Tue Jun 28 16:25:19 2011 +0200
22.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
22.3 @@ -1,24 +0,0 @@
22.4 -{
22.5 -\setlength{\parskip}{3pt plus 3pt minus 3pt} % compact table of contents
22.6 -
22.7 -\tableofcontents
22.8 -
22.9 -\listoffigures
22.10 -%\addcontentsline{toc}{chapter}{List of Figures}
22.11 -
22.12 -{
22.13 -% format sections to chapters for this scope
22.14 -\titleformat{\section}{\bf\huge}{\thesection\quad}{0em}{}
22.15 -\titlespacing*{\section}{0em}{-2em}{1.5em}
22.16 -\def\chapter*#1{\section*{#1}}
22.17 -
22.18 -\vspace*{20mm}
22.19 -\listoftables
22.20 -%\addcontentsline{toc}{chapter}{List of Tables}
22.21 -
22.22 -\vspace*{20mm}
22.23 -\lstlistoflistings
22.24 -%\addcontentsline{toc}{chapter}{List of Listings}
22.25 -}
22.26 -}
22.27 -
23.1 --- a/doc-src/isac/msteger/official_docu/thesis-intro.tex Tue Jun 28 16:25:19 2011 +0200
23.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
23.3 @@ -1,7 +0,0 @@
23.4 -\chapter{Einf\"{u}hrung}
23.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.
23.6 -
23.7 -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.
23.8 -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.
23.9 -
23.10 -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.
24.1 --- a/doc-src/isac/msteger/official_docu/thesis-macros.tex Tue Jun 28 16:25:19 2011 +0200
24.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
24.3 @@ -1,67 +0,0 @@
24.4 -% macros and definitions
24.5 -
24.6 -\newcommand\fname{\begingroup \smaller\urlstyle{tt}\Url}
24.7 -
24.8 -\newcommand\vname{\begingroup \smaller\urlstyle{tt}\Url}
24.9 -
24.10 -
24.11 -% for class names, define our own url style
24.12 -
24.13 -\makeatletter % protect @ names
24.14 -
24.15 -% \url@letstyle: New URL sty to premit break at any letters.
24.16 -% Based on \url@ttstyle
24.17 -
24.18 -\def\Url@letdo{% style assignments for tt fonts or T1 encoding
24.19 -\def\UrlBreaks{\do\a\do\b\do\c\do\d\do\e\do\f\do\g\do\h\do\i\do\j\do\k\do\l%
24.20 - \do\m\do\n\do\o\do\p\do\q\do\r\do\s\do\t\do\u\do\v\do\w\do\x%
24.21 - \do\y\do\z%
24.22 - \do\A\do\B\do\C\do\D\do\E\do\F\do\G\do\H\do\I\do\J\do\K\do\L%
24.23 - \do\M\do\N\do\O\do\P\do\Q\do\R\do\S\do\T\do\U\do\V\do\W\do\X%
24.24 - \do\Y\do\Z%
24.25 -}%
24.26 -\def\UrlBigBreaks{\do\.\do\@\do\\\do\/\do\!\do\_\do\|\do\%\do\;\do\>\do\]%
24.27 - \do\)\do\,\do\?\do\'\do\+\do\=\do\#\do\:\do@url@hyp}%
24.28 -\def\UrlNoBreaks{\do\(\do\[\do\{\do\<}% (unnecessary)
24.29 -\def\UrlSpecials{\do\ {\ }}%
24.30 -\def\UrlOrds{\do\*\do\-\do\~}% any ordinary characters that aren't usually
24.31 -\Urlmuskip = 0mu plus 1mu%
24.32 -}
24.33 -
24.34 -\def\url@letstyle{%
24.35 -\@ifundefined{selectfont}{\def\UrlFont{\sf}}{\def\UrlFont{\sffamily}}\Url@letdo
24.36 -}
24.37 -
24.38 -\makeatother % unprotect @ names
24.39 -
24.40 -
24.41 -\newcommand\cname{\begingroup \smaller\urlstyle{let}\Url}
24.42 -
24.43 -
24.44 -\newcommand{\imgcredit}[1]
24.45 -{%
24.46 -\small
24.47 -[#1]
24.48 -}
24.49 -
24.50 -
24.51 -\newcommand{\chapquote}[2]
24.52 -{%
24.53 -\begin{quote}
24.54 -\emph{%
24.55 -``#1''%
24.56 -}%
24.57 -\begin{flushright}
24.58 -{\scriptsize \sffamily [#2]}%
24.59 -\end{flushright}
24.60 -\end{quote}
24.61 -}
24.62 -
24.63 -
24.64 -% \urlfootnote{url}{day}{month}{year}
24.65 -\newcommand{\murlfootnote}[4]{\footnote{\url{{#1}} (last visit {#4}-{#3}-{#2})}}
24.66 -\newcommand{\murlfootnotebreak}[4]{\footnote{\url{{#1}}\\ \hspace*{6mm}(last visit {#4}-{#3}-{#2})}}
24.67 -
24.68 -% change margin command
24.69 -\def\changemargin#1#2{\list{}{\rightmargin#2\leftmargin#1}\item[]}
24.70 -\let\endchangemargin=\endlist
24.71 \ No newline at end of file
25.1 --- a/doc-src/isac/msteger/official_docu/thesis-preamble.tex Tue Jun 28 16:25:19 2011 +0200
25.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
25.3 @@ -1,183 +0,0 @@
25.4 -\usepackage[ % set page and margin sizes
25.5 - a4paper,
25.6 - twoside=false,
25.7 - top=10mm,
25.8 - bottom=10mm,
25.9 - left=20mm,
25.10 - right=20mm,
25.11 - bindingoffset=10mm,
25.12 - head=10mm,
25.13 - foot=10mm,
25.14 - headsep=10mm,
25.15 - footskip=10mm,
25.16 - includeheadfoot,
25.17 -]{geometry}
25.18 -
25.19 -\usepackage{times} % use PostScript fonts
25.20 -%\usepackage{ngerman} % causes ! Illegal parameter number in definition of \grmn@originalTeX. <to be read again> \penalty l.53 \selectlanguage{austrian}
25.21 -\usepackage{relsize} % relative font sizes \smaller \larger
25.22 -
25.23 -\usepackage[iso-8859-1]{inputenx} % so can use Umlaut chars �, �
25.24 -
25.25 -\usepackage{textcomp} % symbols such as \texttimes and \texteuro
25.26 -
25.27 -\usepackage[bf]{titlesec}
25.28 -% format chapter captions (vorher \Huge)
25.29 -\titleformat{\chapter}{\bf\huge}{\thechapter\quad}{0em}{}
25.30 -\titlespacing*{\chapter}{0em}{-2em}{1.5em}
25.31 -
25.32 -% use caption and subfig (caption2 and subfigure are now obsolete)
25.33 -\usepackage[
25.34 - position=bottom,
25.35 - margin=1cm,
25.36 - font=small,
25.37 - labelfont={bf,sf},
25.38 - format=hang,
25.39 - indention=0mm,
25.40 -]{caption,subfig}
25.41 -
25.42 -\captionsetup[subfigure]{
25.43 - margin=0pt,
25.44 - parskip=0pt,
25.45 - hangindent=0pt,
25.46 - indention=0pt,
25.47 - singlelinecheck=true,
25.48 -}
25.49 -
25.50 -
25.51 -
25.52 -% fancyhdr to make nice headers and footers
25.53 -% and deal with long chapter names
25.54 -
25.55 -\usepackage{fancyhdr} % headers and footers
25.56 -\pagestyle{fancy} % must call to set defaults before redefining
25.57 -
25.58 -\renewcommand{\headrulewidth}{0mm}
25.59 -\renewcommand{\footrulewidth}{0mm}
25.60 -\fancyhf{}
25.61 -
25.62 -\fancyhead[R]{\thepage}
25.63 -
25.64 -\fancyhead[L]{
25.65 - \parbox[t]{0.8\textwidth}{\nouppercase{\leftmark}}
25.66 -}
25.67 -
25.68 -
25.69 -% \usepackage{tabularx} % for better tables
25.70 -\usepackage{multirow}
25.71 -\usepackage{listings} % for listings of source code
25.72 -\usepackage{amsmath}
25.73 -
25.74 -
25.75 -\usepackage[austrian,english]{babel} % load babel *before* natbib or jurabib
25.76 -
25.77 -
25.78 -\usepackage[square]{natbib} % natbib but with my own knat.bst
25.79 - % made with the custom-bib package
25.80 -
25.81 -\usepackage{url}
25.82 -\def\UrlFont{\small\ttfamily}
25.83 -
25.84 -\usepackage{latexsym}
25.85 -
25.86 -\usepackage{color}
25.87 -\definecolor{lightgrey}{gray}{0.8}
25.88 -% \definecolor{darkgreen}{rgb}{0,0.2,0}
25.89 -% \definecolor{darkblue}{rgb}{0,0,0.2}
25.90 -% \definecolor{darkred}{rgb}{0.2,0,0}
25.91 -
25.92 -
25.93 -
25.94 -\usepackage{ifpdf}
25.95 -
25.96 -%begin{latexonly}
25.97 -\ifpdf
25.98 - % pdflatex
25.99 - \usepackage[pdftex]{graphicx}
25.100 - \DeclareGraphicsExtensions{.pdf,.jpg,.png}
25.101 - \pdfcompresslevel=9
25.102 - \pdfpageheight=297mm
25.103 - \pdfpagewidth=210mm
25.104 - \usepackage{rotating} % sidewaystable
25.105 - \usepackage[ % hyperref should be last package loaded
25.106 - pdftex,
25.107 - pdftitle={Automating Test Case Generation from Transition Systems via Symbolic Execution and SAT Solving},
25.108 - pdfsubject={Master's Thesis},
25.109 - pdfauthor={Elisabeth Joebstl},
25.110 - pdfkeywords={Model-Based Testing, Conformance Testing, Automated Test Case Generation, Input Output Symbolic Transition Systems, Symbolic Execution, SMT Solving},
25.111 - bookmarks,
25.112 - bookmarksnumbered,
25.113 - linktocpage,
25.114 - pagebackref,
25.115 - colorlinks,
25.116 - linkcolor=black,
25.117 - anchorcolor=black,
25.118 - citecolor=black,
25.119 - urlcolor=black,
25.120 - pdfview={FitH},
25.121 - pdfstartview={Fit},
25.122 - pdfpagemode=UseOutlines, % open bookmarks in Acrobat
25.123 - plainpages=false, % avoids duplicate page number problem
25.124 - pdfpagelabels, % avoids duplicate page number problem
25.125 - ]{hyperref}
25.126 -
25.127 - \renewcommand*{\backref}[1]{}
25.128 - \renewcommand*{\backrefalt}[4]{
25.129 - \ifcase #1
25.130 - (Not cited.)
25.131 - \or
25.132 - (Cited on page~#2.)
25.133 - \else
25.134 - (Cited on pages~#2.)
25.135 - \fi
25.136 - }
25.137 -
25.138 - \renewcommand*{\backrefsep}{, }
25.139 - \renewcommand*{\backreftwosep}{ and~}
25.140 - \renewcommand*{\backreflastsep}{ and~}
25.141 -
25.142 -\else
25.143 - % latex
25.144 - \usepackage{rotating} % sidewaystable
25.145 - \usepackage{graphicx}
25.146 - \DeclareGraphicsExtensions{.eps}
25.147 -\fi
25.148 -%end{latexonly}
25.149 -
25.150 -
25.151 -% \includeonly{intro,biblio} % selective inclusion
25.152 -
25.153 -
25.154 -
25.155 -\newcommand{\halfh}{9.5cm} % height of figures for 2 per page
25.156 -\newcommand{\thirdh}{6cm} % height of figures for 3 per page
25.157 -
25.158 -
25.159 -\setlength{\parskip}{3pt plus 1pt minus 0pt} % vert. space before a paragraph
25.160 -
25.161 -
25.162 -\setcounter{tocdepth}{2} % lowest section level entered in ToC % TODO FIXXME: wieder auf 1 zurücksetzen?
25.163 -\setcounter{secnumdepth}{2} % lowest section level still numbered
25.164 -
25.165 -
25.166 -\input{thesis-macros}
25.167 -
25.168 -
25.169 -% Reduce vertical distance between items
25.170 -% itemize
25.171 -\let\origitemize\itemize
25.172 -\def\itemize{\origitemize\itemsep0pt}
25.173 -%enumerate
25.174 -\let\origenumerate\enumerate
25.175 -\def\enumerate{\origenumerate\itemsep0pt}
25.176 -
25.177 -
25.178 -% FIXXME: bessere Positionierung der Graphiken
25.179 -%\setcounter{totalnumber}{8}
25.180 -%\setcounter{topnumber}{5}
25.181 -%\setcounter{bottomnumber}{5}
25.182 -
25.183 -%\renewcommand{\topfraction}{0.999}
25.184 -%\renewcommand{\bottomfraction}{0.999}
25.185 -%\renewcommand{\textfraction}{0.0005}
25.186 -
26.1 --- a/doc-src/isac/msteger/official_docu/thesis-title.tex Tue Jun 28 16:25:19 2011 +0200
26.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
26.3 @@ -1,201 +0,0 @@
26.4 -% --- English Title Page ------------------------------------------------
26.5 -\begin{titlepage}
26.6 -\begin{center}
26.7 -\vspace*{8mm}
26.8 -{\LARGE Bachelor's Thesis}\\
26.9 -
26.10 -\vspace{16mm}
26.11 -
26.12 -{\huge \bf Userinterfaces for Computer Theorem Prover\\
26.13 - feasibility study in the Isac-projekt\\}
26.14 -
26.15 -\vspace{16mm}
26.16 -
26.17 -{\LARGE Marco Steger\textsuperscript{1}}\\
26.18 -
26.19 -\vspace{16mm}
26.20 -
26.21 -{\Large
26.22 -Institute for Software Technology (IST)\\
26.23 -Graz University of Technology\\
26.24 -A-8010 Graz, Austria\\}
26.25 -
26.26 -\vspace{16mm}
26.27 -
26.28 -%TODO TU - figure; Line 26, 76
26.29 -%\begin{figure}[!ht]
26.30 -%\centerline{\includegraphics[width=4cm,keepaspectratio=true]{fig/tug}}
26.31 -%\end{figure}
26.32 -
26.33 -\vspace{16mm}
26.34 -
26.35 -{\large
26.36 -\begin{tabular}{ll}
26.37 -Advisor: & Ass.Prof. Dipl.-Ing. Dr.techn.\ Bernhard Aichernig\\[0.5ex]
26.38 -%TODO Aichernig????
26.39 -Co-Advisor: & Dr.techn.\ Walther Neuper
26.40 -\end{tabular}}
26.41 -
26.42 -\vfill
26.43 -{\large Graz, 30.05.2011????}
26.44 -\vspace{15mm}
26.45 -\end{center}
26.46 -
26.47 -\noindent
26.48 -\underline{\hspace*{3cm}}\\
26.49 -{\footnotesize
26.50 -\textsuperscript{1} E-mail: m.steger@student.tugraz.at\\
26.51 -\copyright ~ Copyright 2011 by the author}
26.52 -
26.53 -
26.54 -
26.55 -% --- German Title Page -------------------------------------------------
26.56 -\selectlanguage{austrian}
26.57 -
26.58 -\newpage
26.59 -\begin{center}
26.60 -\vspace*{8mm}
26.61 -{\LARGE Bachelorarbeit}\\
26.62 -
26.63 -\vspace{16mm}
26.64 -
26.65 -{\huge \bf Userinterfaces f\"ur Computer Theorem Prover\\
26.66 - Machbarkeits-Studie im Isac-Projekt\\}
26.67 -
26.68 -\vspace{16mm}
26.69 -
26.70 -{\LARGE Marco Steger\textsuperscript{1}}\\
26.71 -
26.72 -\vspace{16mm}
26.73 -
26.74 -{\Large
26.75 -Institut f\"ur Softwaretechnologie (IST)\\
26.76 -Technische Universit\"at Graz\\
26.77 -A-8010 Graz\\}
26.78 -
26.79 -\vspace{16mm}
26.80 -
26.81 -%\begin{figure}[!ht]
26.82 -%\centerline{\includegraphics[width=4cm,keepaspectratio=true]{fig/tug}}
26.83 -%\end{figure}
26.84 -
26.85 -\vspace{16mm}
26.86 -
26.87 -%TODO Aichernig????
26.88 -{\large
26.89 -\begin{tabular}{ll}
26.90 -Gutachter: & Ass.Prof. Dipl.-Ing. Dr.techn.\ Bernhard Aichernig\\[0.5ex]
26.91 -Mitbetreuer: & Dr.techn.\ Walther Neuper
26.92 -\end{tabular}}
26.93 -
26.94 -\vspace{16mm}
26.95 -{\large Graz, 30.05.2011}
26.96 -
26.97 -\vfill
26.98 -Diese Arbeit ist in deutscher Sprache verfasst.
26.99 -\end{center}
26.100 -
26.101 -\noindent
26.102 -\underline{\hspace*{3cm}}\\
26.103 -{\footnotesize
26.104 -\textsuperscript{1} E-Mail: m.steger@student.tugraz.at\\
26.105 -\copyright ~ Copyright 2011, Marco Steger}
26.106 -\end{titlepage}
26.107 -
26.108 -\selectlanguage{english}
26.109 -
26.110 -
26.111 -% --- English Abstract --------------------------------------------------
26.112 -\pagestyle{plain}
26.113 -\pagenumbering{roman}
26.114 -\newpage
26.115 -
26.116 -\vspace*{25mm}
26.117 -
26.118 -\begin{changemargin}{15mm}{15mm}
26.119 -\begin{center}
26.120 -{\Large\bfseries Abstract}
26.121 -\end{center}
26.122 -\vspace*{7mm}
26.123 -
26.124 -Place english abstract here.
26.125 -
26.126 -\vspace{5mm}
26.127 -\noindent
26.128 -{\large\bfseries Keywords:}
26.129 -some english keywords
26.130 -
26.131 -
26.132 -
26.133 -% --- German Abstract ---------------------------------------------------
26.134 -\selectlanguage{austrian}
26.135 -\newpage
26.136 -
26.137 -\vspace*{10mm}
26.138 -
26.139 -\begin{center}
26.140 -{\Large\bfseries Kurzfassung}
26.141 -\end{center}
26.142 -\vspace*{2mm}
26.143 -
26.144 -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.
26.145 -
26.146 -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.
26.147 -
26.148 -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.
26.149 -
26.150 -\vspace{5mm}
26.151 -\noindent
26.152 -{\large\bfseries Schlagworte:}
26.153 -einige deutsche Schlagworte
26.154 -
26.155 -\selectlanguage{english}
26.156 -\end{changemargin}
26.157 -
26.158 -
26.159 -% --- Pledge ------------------------------------------------------------
26.160 -\newpage
26.161 -\vspace*{20mm}
26.162 -
26.163 -\begin{center}
26.164 -{\Large\bfseries Statutory Declaration}
26.165 -\end{center}
26.166 -\vspace{5mm}
26.167 -\noindent
26.168 -I declare that I have authored this thesis independently, that I have not used other than the declared
26.169 -sources/resources, and that I have explicitly marked all material which has been quoted either
26.170 -literally or by content from the used sources.
26.171 -
26.172 -\vspace{2cm}
26.173 -
26.174 -\noindent
26.175 -\begin{tabular}{ccc}
26.176 -\hspace*{6cm} & \hspace*{2cm} & \hspace*{6.7cm}\\
26.177 -\dotfill & & \dotfill\\
26.178 -place, date & & (signature)\\
26.179 -\end{tabular}
26.180 -
26.181 -\vspace{35mm}
26.182 -
26.183 -
26.184 -\selectlanguage{austrian}
26.185 -
26.186 -\begin{center}
26.187 -{\Large\bfseries Eidesstattliche Erkl\"arung}
26.188 -\end{center}
26.189 -\vspace{5mm}
26.190 -\noindent
26.191 -Ich erkl\"are an Eides statt, dass ich die vorliegende Arbeit selbstst\"andig verfasst, andere als die
26.192 -angegebenen Quellen/Hilfsmittel nicht benutzt, und die den benutzten Quellen w\"ortlich und inhaltlich
26.193 -entnommenen Stellen als solche kenntlich gemacht habe.
26.194 -
26.195 -\vspace{2cm}
26.196 -
26.197 -\noindent
26.198 -\begin{tabular}{ccc}
26.199 -\hspace*{6cm} & \hspace*{2cm} & \hspace*{6.7cm}\\
26.200 -\dotfill & & \dotfill\\
26.201 -Ort, Datum & & (Unterschrift)\\
26.202 -\end{tabular}
26.203 -
26.204 -\selectlanguage{english}
27.1 --- a/doc-src/isac/msteger/official_docu/thesis.tex Tue Jun 28 16:25:19 2011 +0200
27.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
27.3 @@ -1,70 +0,0 @@
27.4 -\documentclass[11pt]{report}
27.5 -%\usepackage{ngerman}
27.6 -\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
27.7 -\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
27.8 -
27.9 -\include{thesis-preamble}
27.10 -
27.11 -\begin{document}
27.12 -
27.13 -\lstset{ % set parameters for listings
27.14 - language=,
27.15 - basicstyle=\small,
27.16 - tabsize=2,
27.17 - xleftmargin=2mm,
27.18 - xrightmargin=2mm,
27.19 - float=htb,
27.20 - frame=shadowbox,
27.21 - framexleftmargin=2mm,
27.22 - rulesepcolor=\color{lightgrey},
27.23 - numbers=left,
27.24 - numberstyle=\scriptsize,
27.25 - extendedchars,
27.26 - breaklines,
27.27 - showtabs=false,
27.28 - showspaces=false,
27.29 - showstringspaces=false,
27.30 - keywordstyle=\bfseries,
27.31 - identifierstyle=\ttfamily,
27.32 - stringstyle=,
27.33 - captionpos=b,
27.34 - abovecaptionskip=\abovecaptionskip,
27.35 - belowcaptionskip=\belowcaptionskip,
27.36 - aboveskip=\floatsep,
27.37 -}
27.38 -
27.39 -
27.40 -%\frontmatter
27.41 -\normalsize
27.42 -\pagestyle{empty} % for title pages
27.43 -
27.44 -\pagenumbering{alph}
27.45 -\include{thesis-title} % Title Pages, Abstracts, Pledge
27.46 -\include{thesis-acknowl} % Acknowledgements
27.47 -\include{thesis-contents} % Table of Contents, List of Figures, List of Tables
27.48 -
27.49 -
27.50 -%\mainmatter
27.51 -\pagestyle{fancy} % for main pages
27.52 -\pagenumbering{arabic} % for main pages
27.53 -
27.54 -\include{thesis-intro} % Introduction
27.55 -\include{Doku}
27.56 -% \include{your main files}
27.57 -
27.58 -%\include{thesis-conclusion} % Conclusion and Future Work
27.59 -
27.60 -
27.61 -\appendix
27.62 -% \noappendicestocpagenum
27.63 -% \addappheadtotoc
27.64 -
27.65 -\include{thesis-appendix} % Appendix A
27.66 -
27.67 -
27.68 -%\backmatter
27.69 -\include{thesis-biblio} % Bibliography
27.70 -% \include{glossary} % Glossary
27.71 -% \include{index} % Index
27.72 -
27.73 -\end{document}
27.74 \ No newline at end of file
28.1 --- a/src/Tools/jEditC/build/.scala_dependencies Tue Jun 28 16:25:19 2011 +0200
28.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
28.3 @@ -1,24 +0,0 @@
28.4 -/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/Pure.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/cobra.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/js.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/ErrorList.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/Hyperlinks.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/SideKick.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/Console.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/scala-compiler.jar:/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jedit.jar:/usr/share/scala/lib/jline.jar:/usr/share/scala/lib/scala-compiler.jar:/usr/share/scala/lib/scala-dbc.jar:/usr/share/scala/lib/scala-library.jar:/usr/share/scala/lib/scala-partest.jar:/usr/share/scala/lib/scala-swing.jar:/usr/share/scala/lib/scalacheck.jar:/usr/share/scala/lib/scalap.jar:/home/gadei/isac/isa/src/Tools/jEditC/build/classes
28.5 --------
28.6 -../src/testSD.scala -> ../src/testSD.scala
28.7 -../src/testSD.scala -> ../src/testSDToolPanel.scala
28.8 -../src/testSD.scala -> ../src/testSDOptionPane.scala
28.9 -../src/testSD.scala -> ../src/testSDPlugin.scala
28.10 -../src/testSD.scala -> ../src/testSDTextArea.scala
28.11 -../src/testSDPlugin.scala -> ../src/testSDPlugin.scala
28.12 -../src/testSDOptionPane.scala -> ../src/testSDOptionPane.scala
28.13 -../src/testSDOptionPane.scala -> ../src/testSDPlugin.scala
28.14 -../src/testSDToolPanel.scala -> ../src/testSD.scala
28.15 -../src/testSDToolPanel.scala -> ../src/testSDToolPanel.scala
28.16 -../src/testSDToolPanel.scala -> ../src/testSDPlugin.scala
28.17 --------
28.18 -../src/testSD.scala -> classes/testSD.class
28.19 -../src/testSDPlugin.scala -> classes/testSDPlugin.class
28.20 -../src/testSDPlugin.scala -> classes/testSDPlugin$.class
28.21 -../src/testSDTextArea.scala -> classes/testSDTextArea.class
28.22 -../src/testSDOptionPane.scala -> classes/testSDOptionPane.class
28.23 -../src/testSDActions.scala -> classes/testSDActions.class
28.24 -../src/testSDToolPanel.scala -> classes/testSDToolPanel.class
28.25 -../src/testSDToolPanel.scala -> classes/testSDToolPanel$$anon$2.class
28.26 -../src/testSDToolPanel.scala -> classes/testSDToolPanel$$anon$1.class
28.27 -../src/testSDToolPanel.scala -> classes/testSDToolPanel$$anon$3.class
29.1 --- a/src/Tools/jEditC/nbproject/private/private.properties Tue Jun 28 16:25:19 2011 +0200
29.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
29.3 @@ -1,9 +0,0 @@
29.4 -application.args=-noserver -nobackground
29.5 -compile.on.save=false
29.6 -do.depend=false
29.7 -do.jar=true
29.8 -file.reference.isabelle-jedit-src=/home/gadei/isac/isa/src/Tools/jEditC/src
29.9 -file.reference.Pure.jar=/home/gadei/isac/isa/contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/Pure.jar
29.10 -javac.debug=true
29.11 -javadoc.preview=true
29.12 -user.properties.file=/home/gadei/.netbeans/6.9/build.properties