116 \begin{center} |
116 \begin{center} |
117 {\Large\bfseries Abstract} |
117 {\Large\bfseries Abstract} |
118 \end{center} |
118 \end{center} |
119 \vspace*{7mm} |
119 \vspace*{7mm} |
120 |
120 |
121 Place english abstract here. |
121 The computer theorem prover Isabelle switches from a user interface for expert users to a user interface which is more powerful and which serves integration of Isabelle into other tools for software engineers. |
|
122 |
|
123 This bachelor thesis in ``Telematik'' introduces the specific components underlying Isabelle's new user interface, the scala-layer for asyncronous editing of proof documents, the Java-based editor jEdit together with the respective plugin mechanisms; and the thesis documents the current organization of these components in Isabelle and sets up the whole system, Isabelle, Scala and jEdit in the IDE NetBeans copying the configuration of the Isabelle developer team. This setup is explored in the implementation of a test-plugin, and the experiences are documented in detail. |
|
124 |
|
125 Thus the prerequisites are given for cooperation in the further development of Isabelle's future front-end and respective integration into development tools like test case generators for software engineers. |
122 |
126 |
123 \vspace{5mm} |
127 \vspace{5mm} |
124 \noindent |
128 \noindent |
125 {\large\bfseries Keywords:} |
129 {\large\bfseries Keywords:} |
126 some english keywords |
130 computer theorem prover, Isabelle, user-interface, jEdit, plugin, Scala, actors, asynconous communication, proof document, structured derivations |
127 |
131 |
128 |
132 |
129 |
133 |
130 % --- German Abstract --------------------------------------------------- |
134 % --- German Abstract --------------------------------------------------- |
131 \selectlanguage{austrian} |
135 \selectlanguage{austrian} |
138 \end{center} |
142 \end{center} |
139 \vspace*{2mm} |
143 \vspace*{2mm} |
140 |
144 |
141 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. |
145 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. |
142 |
146 |
143 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. |
147 Die vorliegende Bachelorarbeit in Telematik f\"uhrt in die speziellen, dem Frontend zugrundleliegenden Konzepte und Komponenten (Scala-Layer f\"ur asynchrone Bearbeitung von Beweisdokumenten, jEdit mit Plugins, Parser) ein, dokumentiert die momentane Organisation dieser Komponenten im Isabelle System und setzt das gesamte System in einer integrierten Entwicklungsungebung auf. Dieses Setup wird in der Implementation eines Test-Plugins erprobt. Die Erfahrungen mit diesem Test werden ausf\"uhrlich dokumentiert. |
144 |
148 |
145 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. |
149 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. |
146 |
150 |
147 \vspace{5mm} |
151 \vspace{5mm} |
148 \noindent |
152 \noindent |
149 {\large\bfseries Schlagworte:} |
153 {\large\bfseries Schlagworte:} |
150 einige deutsche Schlagworte |
154 Computer Theorem Proving, Isabelle, User-Interface, jEdit, Plugin, Scala, Actors, Asyncrone Kommunikation, Beweis-Dokument, Structured Derivations |
151 |
155 |
152 \selectlanguage{english} |
156 \selectlanguage{english} |
153 \end{changemargin} |
157 \end{changemargin} |
154 |
158 |
155 |
159 |