intermed. msteger bakk-presentation.tex
did not get rid of fig/
1 % /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex
7 \setbeamercovered{transparent}
9 \usepackage[english]{babel}
10 \usepackage[latin1]{inputenc}
13 \usepackage[T1]{fontenc}
14 %\usepackage{graphicx}
16 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
17 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
19 \title[Isabelle Frontend]
20 {Userinterfaces \\f\"ur Computer Theorem Prover,\\
21 Machbarkeits-Studie im \isac-Projekt
23 \subtitle{Bachelorarbeit Telematik}
26 \institute{Institut f\"ur Software Technologie\\
27 Technische Universit\"at Graz}
30 %\subject{Formal specification of math assistants}
31 % This is only inserted into the PDF information catalog
33 % Delete this, if you do not want the table of contents to pop up at
34 % the beginning of each subsection:
39 \tableofcontents[currentsection,currentsubsection]
44 % If you wish to uncover everything in a step-wise fashion, uncomment
45 % the following command:
46 %\beamerdefaultoverlayspecification{<+->}
57 % You might wish to add the option [pausesections]
60 \section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}
61 \subsection[Isabelle]{Der Theoremprover Isabelle}
63 \frametitle{Der Theoremprover Isabelle}
65 \item Anwendungen von Isabelle
67 \item Mechanisieren von Mathematik Theorien
69 \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots
70 \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots
71 \item High Order Logics, Logic of Computable Functions, \dots
74 \item Math.Grundlagen f\"ur Softwaretechnologie
76 \item Hoare Logic, Temporal Logic of Actions, Hoare for Java
77 \item Theory for Unix file-system security, for state spaces, \dots
78 \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}
82 \item Integration von Isabelle in Entwicklungstools
84 \item Boogie --- Verification Condition Generator
85 \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs
86 \item Test Case Generators (TUG) ?
89 \item Isar, die Beweissprache von Isabelle
91 \item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$
93 \alert{Beweisteile asynchron interpretiert}
98 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers}
99 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
102 \includegraphics[width=100mm]{fig-reuse-ml-scala-SD}
104 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
105 \label{fig-reuse-ml-scala}
109 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML}
111 \item Das Protokoll ist \textbf{asynchron}: \\
112 verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert
114 \item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen)
116 \item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\
118 Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\
120 Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\
122 \alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}}
126 \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}
127 \begin{frame}\frametitle{Isabelle Files: *.jar}
129 ----- for ``isabelle jedit \&''; contained in Isabelle\_bundle}\\
131 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar\\
132 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar\\
133 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar\\
134 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar\\
135 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \alert{$\;\;\;\;\;\;\;\;\;\;\;\Longleftarrow$ entry to SML}\\
136 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar\\
137 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar\\
138 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar\\
139 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar\\
140 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar\\
141 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar\\
142 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar\\
143 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar\\
144 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar\\
145 ./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar\\
148 ----- scala system; contained in Isabelle\_bundle}\\
149 ./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar\\
150 ./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar\\
151 ./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar\\
152 ./contrib/scala-2.8.1.final/lib/scala-compiler.jar\\
153 ./contrib/scala-2.8.1.final/lib/scalap.jar\\
154 ./contrib/scala-2.8.1.final/lib/scala-swing.jar\\
155 ./contrib/scala-2.8.1.final/lib/scala-library.jar\\
156 ./contrib/scala-2.8.1.final/lib/jline.jar\\
157 ./contrib/scala-2.8.1.final/lib/scala-dbc.jar\\
158 ./contrib/scala-2.8.1.final/src/scala-library-src.jar\\
159 ./contrib/scala-2.8.1.final/src/scala-swing-src.jar\\
160 ./contrib/scala-2.8.1.final/src/scala-compiler-src.jar\\
161 ./contrib/scala-2.8.1.final/src/scala-dbc-src.jar\\
162 ./contrib/scala-2.8.1.final/src/sbaz-src.jar\\
166 \begin{frame}\frametitle{Isabelle Files: *.scala}
168 ./src/Pure/General/xml.scala\\
169 ./src/Pure/General/linear\_set.scala\\
170 ./src/Pure/General/symbol.scala\\
171 ./src/Pure/General/exn.scala\\
172 ./src/Pure/General/position.scala\\
173 ./src/Pure/General/scan.scala\\
174 ./src/Pure/General/xml\_data.scala\\
175 ./src/Pure/General/yxml.scala\\
176 ./src/Pure/General/markup.scala\\
177 ./src/Pure/General/sha1.scala\\
178 ./src/Pure/General/timing.scala\\
179 ./src/Pure/General/pretty.scala\\
181 ./src/Pure/Concurrent/volatile.scala\\
182 ./src/Pure/Concurrent/future.scala\\
183 ./src/Pure/Concurrent/simple\_thread.scala\\
185 ./src/Pure/Thy/html.scala\\
186 ./src/Pure/Thy/completion.scala\\
187 ./src/Pure/Thy/thy\_header.scala\\
188 ./src/Pure/Thy/thy\_syntax.scala\\
189 ./src/Pure/Isac/isac.scala\\
190 ./src/Pure/library.scala\\
192 ./src/Pure/Isar/keyword.scala\\
193 ./src/Pure/Isar/outer\_syntax.scala\\
194 ./src/Pure/Isar/token.scala\\
195 ./src/Pure/Isar/parse.scala\\
197 ./src/Pure/System/gui\_setup.scala\\
198 ./src/Pure/System/isabelle\_system.scala\\
199 ./src/Pure/System/swing\_thread.scala\\
200 ./src/Pure/System/download.scala\\
201 ./src/Pure/System/session\_manager.scala\\
202 ./src/Pure/System/standard\_system.scala\\
203 ./src/Pure/System/isabelle\_syntax.scala\\
204 ./src/Pure/System/session.scala\\
205 ./src/Pure/System/platform.scala\\
206 ./src/Pure/System/cygwin.scala\\
207 ./src/Pure/System/event\_bus.scala\\
208 ./src/Pure/System/isabelle\_process.scala\\
210 ./src/Pure/PIDE/document.scala\\
211 ./src/Pure/PIDE/markup\_tree.scala\\
212 ./src/Pure/PIDE/text.scala\\
213 ./src/Pure/PIDE/command.scala\\
214 ./src/Pure/PIDE/isar\_document.scala
218 \begin{frame}\frametitle{*.scala --- *.ML}
220 isabisac\$ ls -l src/Pure/System/\\
221 -rw-r--r-- 1 msteger root 3987 2011-03-14 17:09 cygwin.scala\\
222 -rw-r--r-- 1 msteger root 1486 2011-03-14 17:09 download.scala\\
223 -rw-r--r-- 1 msteger root 1296 2011-03-14 17:09 event\_bus.scala\\
224 -rw-r--r-- 1 msteger root 1830 2011-03-14 17:09 gui\_setup.scala\\
225 -rw-r--r-- 1 msteger root 5722 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{ML}\\
226 -rw-r--r-- 1 msteger root 1059 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{scala}\\
227 -rw-r--r-- 1 msteger root 1659 2011-03-14 17:09 isabelle\_syntax.scala\\
228 -rw-r--r-- 1 msteger root 2087 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{ML}\\
229 -rw-r--r-- 1 msteger root 1168 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{scala}\\
230 -rw-r--r-- 1 msteger root 5935 2011-03-14 17:09 isar.ML\\
231 -rw-r--r-- 1 msteger root 1989 2011-03-14 17:09 platform.scala\\
232 -rw-r--r-- 1 msteger root 1427 2011-03-14 17:09 session\_manager.scala\\
233 -rw-r--r-- 1 msteger root 3833 2011-03-14 17:09 \alert{session}.\textbf{ML}\\
234 -rw-r--r-- 1 msteger root 9172 2011-03-14 17:09 \alert{session}.\textbf{scala}\\
235 -rw-r--r-- 1 msteger root 9086 2011-03-14 17:09 standard\_system.scala\\
236 -rw-r--r-- 1 msteger root 1643 2011-03-14 17:09 swing\_thread.scala\\
241 \subsection[jEdit]{Das Frontend: jEdit und ``plugins''}
242 \begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''}
244 \item \textbf{jEdit} \textit{``is a mature programmer's text editor with hundreds (counting the time developing \textbf{plugins}) of person-years of development behind it.''}
246 \item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt
248 \item Isabelle verwendet eine Reihe davon
250 \item der Parser ``Sidekick''
251 \item Console f\"ur jEdit-Komponenten
257 \item jEdit ist ``open source'' mit gro\3er Community
259 \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle
263 \section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)}
264 \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}
265 \begin{frame}\frametitle{Definition der Aufgabenstellung}
266 Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured derivations'' in Isabelle.\\
268 \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\
272 \item Relevante Isabelle Komponenten identifizieren und studieren
273 \item Installation der Standard-Komponenten
274 \item Entwicklungsumgebung vom Isabelle-Team kopieren
275 \item Relevante Komponenten implementieren
277 \item jEdit Plugin f\"ur SD
278 \item zugeh\"origen Parser
279 \item nicht vorgesehen: SD-Interpreter in Isar (SML)
284 %\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
285 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}
288 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
289 \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
290 \> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
291 \>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
292 \> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
293 \>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
294 \> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
295 \> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
296 \> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
297 \> \>$\equiv$\>\vdots\\
298 \> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
299 \> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
300 \> \> \>$1 + -1 * x$\\
301 \>\dots\>$1 + -1 * x$\\
302 \>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
308 \subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE}
309 \begin{frame}\frametitle{Konfiguration in NetBeans}
310 Mehrere Run-Konfigurationen sind praktisch:
312 \item Start von jEdit + Plug-ins aus NetBeans
314 \item Exekution der fertig kompilierten jEdit.jar
315 \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen !
317 \item Start von jEdit aus der Konsole
319 \vspace{0.2cm} \pause
320 Dementsprechend komplex sind die Konfigurations-Files:
322 \begin{tabular}{l r l}
323 build.xml & 102 & LOCs\\
324 project.xml & 25 & LOCs\\
325 project.properties & 85 & LOCs\\
326 build-impl.xml & 708 & LOCs\\
327 & & (teilw. automatisch generiert)\end{tabular}
331 \subsection[Implementation]{Komponenten zur Implementation von SD}
333 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
335 \includegraphics[width=100mm]{fig-jedit-plugins-SD}
336 \label{Frontend des jEdit}
340 \begin{frame}\frametitle{jEdit-Plugin}
342 \item Aufbau: Ein Plugin besteht aus:
345 \item Source-Files: \textbf{Scala}
349 \item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)
352 %\item Bestehendes Java-Plugin in Scala transferieren
354 %\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren
358 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}
359 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:
362 \item Grunds\"atzlicher Aufbau eines GUIs
364 \item Kopieren von Text zwischen den einzelnen Buffers
367 \item \alert{Somit auch Zugriff auf andere Plugins!}
370 \item Ansatz f\"ur die Einbindung des SD-Parsers
373 \item Zugriff auf Isabelle-Pure: \alert{parsen von SD parallel zu Isabelle/Isar}
381 \subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
383 \section[Summary]{Zusammenfassung}
384 \begin{frame}\frametitle{Zusammenfassung}
385 Folgende Milestones wurden erfolgreich abgeschlossen:
387 \item Relevante Isabelle Komponenten dokumentiert (...Std.)
388 \item Installation der Standard-Komponenten:
390 \item Mercurial Versioncontrol
392 \item Standard Isabelle Bundle
394 \item Entwicklungsumgebung vom Isabelle-Team kopieren
396 \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
397 \item jEdit als NetBeans Projekt definiert
399 \item Relevante Komponenten implementieren
401 \item jEdit Plugin f\"ur SD
402 \item Verbindung des Plugins zu Isabelle
403 \item zugeh\"origen Parser: nur ein Test in SML
408 \begin{frame}\frametitle{Zusammenfassung}
410 \alert{$\mathbf{- - -}$}\\
411 Aus Zeitgr\"unden nicht m\"oglich: ein komplettes SD-Plugin;\\
412 dazu w\"are auch ein Interpreter auf der ML-Seite n\"otig.\\
414 \alert{$\mathbf{+ + +}$}\\
415 Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen:
417 \item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
418 \item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend
419 \item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).
423 \begin{frame}\frametitle{}
425 \LARGE{Danke f\"ur die Aufmerksamkeit !}