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[Isabelle]{Einleitung: Der Theoremprover Isabelle}
62 \frametitle{Der Theoremprover Isabelle}
64 \item Anwendungen von Isabelle
66 \item Mechanisieren von Mathematik Theorien
68 \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots
69 \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots
70 \item High Order Logics, Logic of Computable Functions, \dots
73 \item Math.Grundlagen f\"ur Softwaretechnologie
75 \item Hoare Logic, Temporal Logic of Actions, Hoare for Java
76 \item Theory for Unix file-system security, for state spaces, \dots
77 \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}
81 \item Integration von Isabelle in Entwicklungstools
83 \item Boogie --- Verification Condition Generator
84 \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs
85 \item Test Case Generators (TUG) ?
88 \item Isar, die Beweissprache von Isabelle
90 \item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$
92 \alert{Beweisteile asynchron interpretiert}
97 \section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}
98 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers}
99 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
102 %\includegraphics[width=75mm]{fig/archi/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]{Projektarbeit: Vorbereitungen f\"ur ``structured derivations''}
264 \subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
265 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}
268 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
269 \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
270 \> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
271 \>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
272 \> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
273 \>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
274 \> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
275 \> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
276 \> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
277 \> \>$\equiv$\>\vdots\\
278 \> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
279 \> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
280 \> \> \>$1 + -1 * x$\\
281 \>\dots\>$1 + -1 * x$\\
282 \>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
288 \subsection[NetBeans]{Aufsetzen des Projektes in der NetBeans IDE}
289 \begin{frame}\frametitle{Grundlegender Aufbau eines jEdit-Plugin}
291 \item Ein Plugin besteht aus:
294 \item Source-Files: \textbf{Scala}
298 \item XML-Files: \textit{Klebstoff} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)
301 \item Bestehendes Java-Plugin in Scala transferieren
303 \item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren
307 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
310 \includegraphics[width=75mm]{fig/block-frontend}
312 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
313 \label{Frontend des jEdit}
317 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}
318 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:
321 \item Grunds\"atzlicher Aufbau eines GUIs
323 \item Kopieren von Text zwischen den einzelnen Buffern
326 \item \alert{Somit auch Zugriff auf andere Plugins!}
329 \item Ansatz f\"ur die Einbindung des SD-Parsers
332 \item Zugriff auf Isabelle-Pure: \alert{parsen von SD parallel zu Isabelle/Isar}
339 \subsection[Implementation]{Komponenten zur von SD}
340 \subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
342 \section[Summary]{Zusammenfassung}
343 \begin{frame}\frametitle{Zusammenfassung}
347 \begin{frame}\frametitle{}