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}\;\;\;$
92 \item Demo 'Allgemeine Dreiecke'
94 \alert{Beweisteile asynchron interpretiert}
99 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers}
100 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
103 \includegraphics[width=100mm]{fig-reuse-ml-scala-SD}
105 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
106 \label{fig-reuse-ml-scala}
110 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML}
112 \item Das Protokoll ist \textbf{asynchron}: \\
113 verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert
115 \item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen)
117 \item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\
119 Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\
121 Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\
123 \alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}}
127 \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}
130 \begin{frame}\frametitle{Isabelle Files: *.scala}
132 \textbf{\$ find -name ``*.scala''}\\
133 ./src/Pure/General/xml.scala\\
134 ./src/Pure/General/linear\_set.scala\\
136 ./src/Pure/General/symbol.scala\\
137 ./src/Pure/General/exn.scala\\
138 ./src/Pure/General/position.scala\\
139 ./src/Pure/General/scan.scala\\
140 ./src/Pure/General/xml\_data.scala\\
141 ./src/Pure/General/yxml.scala\\
142 ./src/Pure/General/markup.scala\\
144 ./src/Pure/General/sha1.scala\\
145 ./src/Pure/General/timing.scala\\
146 ./src/Pure/General/pretty.scala\\
148 ./src/Pure/Concurrent/volatile.scala\\
149 ./src/Pure/Concurrent/future.scala\\
150 ./src/Pure/Concurrent/simple\_thread.scala\\
152 ./src/Pure/Thy/html.scala\\
153 ./src/Pure/Thy/completion.scala\\
154 ./src/Pure/Thy/thy\_header.scala\\
155 ./src/Pure/Thy/thy\_syntax.scala\\
156 ./src/Pure/Isac/isac.scala\\
157 ./src/Pure/library.scala\\
159 ./src/Pure/Isar/keyword.scala\\
160 ./src/Pure/Isar/outer\_syntax.scala\\
161 ./src/Pure/Isar/token.scala\\
162 ./src/Pure/Isar/parse.scala\\
164 ./src/Pure/System/gui\_setup.scala\\
165 ./src/Pure/System/isabelle\_system.scala\\
166 ./src/Pure/General/timing.scala\\
167 ./src/Pure/General/pretty.scala\\
169 ./src/Pure/Concurrent/volatile.scala\\
170 ./src/Pure/Concurrent/future.scala\\
171 ./src/Pure/Concurrent/simple\_thread.scala\\
173 ./src/Pure/Thy/html.scala\\
174 ./src/Pure/Thy/completion.scala\\
175 ./src/Pure/Thy/thy\_header.scala\\
176 ./src/Pure/Thy/thy\_syntax.scala\\
177 ./src/Pure/Isac/isac.scala\\
178 ./src/Pure/library.scala\\
180 ./src/Pure/Isar/keyword.scala\\
181 ./src/Pure/Isar/outer\_syntax.scala\\
182 ./src/Pure/Isar/token.scala\\
183 ./src/Pure/Isar/parse.scala\\
185 ./src/Pure/System/gui\_setup.scala\\
186 ./src/Pure/System/isabelle\_system.scala\\
187 ./src/Pure/System/swing\_thread.scala\\
188 ./src/Pure/System/download.scala\\
189 ./src/Pure/System/session\_manager.scala\\
190 ./src/Pure/System/standard\_system.scala\\
191 ./src/Pure/System/isabelle\_syntax.scala\\
192 ./src/Pure/System/session.scala\\
193 ./src/Pure/System/platform.scala\\
194 ./src/Pure/System/cygwin.scala\\
195 ./src/Pure/System/event\_bus.scala\\
196 ./src/Pure/System/isabelle\_process.scala\\
198 ./src/Pure/PIDE/document.scala\\
199 ./src/Pure/PIDE/markup\_tree.scala\\
200 ./src/Pure/PIDE/text.scala\\
201 ./src/Pure/PIDE/command.scala\\
202 ./src/Pure/PIDE/isar\_document.scala
208 \subsection[jEdit]{Das Frontend: jEdit und ``plugins''}
209 \begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''}
211 \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.''}
213 \item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt
215 \item Isabelle verwendet eine Reihe davon
217 \item der Parser ``Sidekick''
218 \item Console f\"ur jEdit-Komponenten
224 \item jEdit ist ``open source'' mit gro\3er Community
226 \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle
230 \section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)}
231 \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}
232 \begin{frame}\frametitle{Definition der Aufgabenstellung}
233 Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured~derivations'' (SD) in Isabelle.\\
235 \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\
239 \item Relevante Isabelle Komponenten identifizieren und studieren
240 \item Installation der Standard-Komponenten
241 \item Entwicklungsumgebung vom Isabelle-Team kopieren
242 \item Relevante Komponenten implementieren
244 \item jEdit Plugin f\"ur SD
245 \item zugeh\"origen Parser
246 \item nicht vorgesehen: SD-Interpreter in Isar (SML)
251 %\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
252 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}
255 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
256 \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
257 \> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
258 \>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
259 \> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
260 \>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
261 \> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
262 \> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
263 \> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
264 \> \>$\equiv$\>\vdots\\
265 \> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
266 \> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
267 \> \> \>$1 + -1 * x$\\
268 \>\dots\>$1 + -1 * x$\\
269 \>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
275 \subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE}
276 \begin{frame}\frametitle{Konfiguration in NetBeans}
277 Mehrere Run-Konfigurationen sind praktisch:
279 \item Start von jEdit + Plug-ins aus NetBeans
281 \item Exekution der fertig kompilierten jEdit.jar
282 \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen !
284 \item Start von jEdit aus der Konsole
286 \vspace{0.2cm} \pause
287 Dementsprechend komplex sind die Konfigurations-Files:
289 \begin{tabular}{l r l}
290 build.xml & 102 & LOCs\\
291 project.xml & 25 & LOCs\\
292 project.properties & 85 & LOCs\\
293 build-impl.xml & 708 & LOCs\\
294 & & (teilw. automatisch generiert)\end{tabular}
298 \subsection[Implementation]{Komponenten zur Implementation von SD}
300 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
302 \includegraphics[width=100mm]{fig-jedit-plugins-SD}
303 \label{Frontend des jEdit}
307 \begin{frame}\frametitle{jEdit-Plugin}
309 \item Aufbau: Ein Plugin besteht aus:
312 \item Source-Files: \textbf{Scala}
316 \item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)
319 %\item Bestehendes Java-Plugin in Scala transferieren
321 %\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren
325 \begin{frame}\frametitle{Sources des jEdit Plugins}
327 src/Tools/jEditC\textbf{\$ ls -l *}\\
335 \textbf{plugin/}build.xml\\
336 \textbf{plugin/}changes40.txt\\
337 \textbf{plugin/}changes42.txt\\
338 \textbf{plugin/}description.html\\
339 \textbf{plugin/}IsacActions.java\\
340 \textbf{plugin/}Isac.iml\\
341 \textbf{plugin/}Isac.java\\
342 \textbf{plugin/}IsacOptionPane.java\\
343 \textbf{plugin/}IsacPlugin.java\\
344 \textbf{plugin/}IsacTextArea.java\\
345 \textbf{plugin/}IsacToolPanel.java\\
346 \textbf{plugin/}plugin\\
347 \textbf{plugin/}README.txt\\
348 \textbf{nbproject/*}\\
349 \textbf{src/}actions.xml\\
350 \textbf{src/}changes40.txt\\
351 \textbf{src/}changes42.txt\\
352 \textbf{src/}description.html\\
353 \textbf{src/}dockables.xml\\
354 \textbf{src/}IsacActions.scala\\
355 \textbf{src/}Isac.iml\\
356 \textbf{src/}IsacOptionPane.scala\\
357 \textbf{src/}IsacPlugin.scala\\
358 \textbf{src/}Isac.props\\
359 \textbf{src/}Isac.scala\\
360 \textbf{src/}IsacTextArea.scala\\
361 \textbf{src/}IsacToolPanel.scala\\
362 \textbf{src/}manifest.mf\\
363 \textbf{src/}README.txt\\
364 \textbf{src/}users-guide.xml
368 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}
369 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:
372 \item Grunds\"atzlicher Aufbau eines GUIs
374 \item Kopieren von Text zwischen den einzelnen Buffers
377 \item \alert{Somit auch Zugriff auf andere Plugins!}
380 \item Ansatz f\"ur die Einbindung des SD-Parsers
383 \item Zugriff auf Isabelle-Pure: \alert{parsen von SD parallel zu Isabelle/Isar}
391 %\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
393 \section[Summary]{Zusammenfassung}
394 \begin{frame}\frametitle{Zusammenfassung}
395 Folgende Milestones wurden erfolgreich abgeschlossen:
397 \item Relevante Isabelle Komponenten dokumentiert
399 \item Installation der Standard-Komponenten:
401 \item Mercurial Versioncontrol
403 \item Standard Isabelle Bundle
406 \item Entwicklungsumgebung vom Isabelle-Team kopieren
408 \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
409 \item jEdit als NetBeans Projekt definiert
412 \item Relevante Komponenten implementieren
414 \item jEdit Plugin f\"ur SD
415 \item Verbindung des Plugins zu Isabelle
416 \item zugeh\"origen Parser: nur ein Test in SML
421 \begin{frame}\frametitle{Zusammenfassung}
423 \alert{$\mathbf{- - -}$}\\
424 Aus Zeitgr\"unden nicht m\"oglich: ein komplettes SD-Plugin;\\
425 dazu w\"are auch ein Interpreter auf der ML-Seite n\"otig.\\
427 \alert{$\mathbf{+ + +}$}\\
429 Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen:
431 \item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
432 \item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend
433 \item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).
437 \begin{frame}\frametitle{}
439 \LARGE{Danke f\"ur die Aufmerksamkeit !}