|
1 % /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex |
|
2 |
|
3 \documentclass{beamer} |
|
4 \mode<presentation> |
|
5 { |
|
6 \usetheme{Hannover} |
|
7 \setbeamercovered{transparent} |
|
8 } |
|
9 \usepackage[english]{babel} |
|
10 \usepackage[latin1]{inputenc} |
|
11 \usepackage{times} |
|
12 \usepackage{ngerman} |
|
13 \usepackage[T1]{fontenc} |
|
14 %\usepackage{graphicx} |
|
15 |
|
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}$}} |
|
18 |
|
19 \title[Isabelle Frontend] |
|
20 {Userinterfaces \\f\"ur Computer Theorem Prover,\\ |
|
21 Machbarkeits-Studie im \isac-Projekt |
|
22 } |
|
23 \subtitle{Bachelorarbeit Telematik} |
|
24 |
|
25 \author{Marco Steger} |
|
26 \institute{Institut f\"ur Software Technologie\\ |
|
27 Technische Universit\"at Graz} |
|
28 |
|
29 \date{21.06.2011} |
|
30 %\subject{Formal specification of math assistants} |
|
31 % This is only inserted into the PDF information catalog |
|
32 |
|
33 % Delete this, if you do not want the table of contents to pop up at |
|
34 % the beginning of each subsection: |
|
35 \AtBeginSubsection[] |
|
36 { |
|
37 \begin{frame}<beamer> |
|
38 \frametitle{Outline} |
|
39 \tableofcontents[currentsection,currentsubsection] |
|
40 \end{frame} |
|
41 } |
|
42 |
|
43 |
|
44 % If you wish to uncover everything in a step-wise fashion, uncomment |
|
45 % the following command: |
|
46 %\beamerdefaultoverlayspecification{<+->} |
|
47 |
|
48 |
|
49 \begin{document} |
|
50 \begin{frame} |
|
51 \titlepage |
|
52 \end{frame} |
|
53 |
|
54 \begin{frame} |
|
55 \frametitle{Outline} |
|
56 \tableofcontents |
|
57 % You might wish to add the option [pausesections] |
|
58 \end{frame} |
|
59 |
|
60 \section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end} |
|
61 \subsection[Isabelle]{Der Theoremprover Isabelle} |
|
62 \begin{frame} |
|
63 \frametitle{Der Theoremprover Isabelle} |
|
64 \begin{itemize} |
|
65 \item Anwendungen von Isabelle |
|
66 \begin{itemize} |
|
67 \item Mechanisieren von Mathematik Theorien |
|
68 \begin{itemize} |
|
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 |
|
72 \end{itemize} |
|
73 \pause |
|
74 \item Math.Grundlagen f\"ur Softwaretechnologie |
|
75 \begin{itemize} |
|
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} |
|
79 \end{itemize} |
|
80 \end{itemize} |
|
81 \pause |
|
82 \item Integration von Isabelle in Entwicklungstools |
|
83 \begin{itemize} |
|
84 \item Boogie --- Verification Condition Generator |
|
85 \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs |
|
86 \item Test Case Generators (TUG) ? |
|
87 \end{itemize} |
|
88 \pause |
|
89 \item Isar, die Beweissprache von Isabelle |
|
90 \begin{itemize} |
|
91 %\item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$ |
|
92 \item Demo 'Allgemeine Dreiecke' |
|
93 \pause |
|
94 \alert{Beweisteile asynchron interpretiert} |
|
95 \end{itemize} |
|
96 \end{itemize} |
|
97 \end{frame} |
|
98 |
|
99 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers} |
|
100 \begin{frame}\frametitle{Die Konzeption des Scala-Layers} |
|
101 \begin{figure} |
|
102 \begin{center} |
|
103 \includegraphics[width=100mm]{fig-reuse-ml-scala-SD} |
|
104 \end{center} |
|
105 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.} |
|
106 \label{fig-reuse-ml-scala} |
|
107 \end{figure} |
|
108 \end{frame} |
|
109 |
|
110 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML} |
|
111 \begin{itemize} |
|
112 \item Das Protokoll ist \textbf{asynchron}: \\ |
|
113 verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert |
|
114 \pause |
|
115 \item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen) |
|
116 \pause |
|
117 \item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\ |
|
118 \pause |
|
119 Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\ |
|
120 \pause |
|
121 Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\ |
|
122 \pause |
|
123 \alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}} |
|
124 \end{itemize} |
|
125 \end{frame} |
|
126 |
|
127 \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium} |
|
128 |
|
129 |
|
130 \begin{frame}\frametitle{Isabelle Files: *.scala} |
|
131 {\tiny |
|
132 \textbf{\$ find -name ``*.scala''}\\ |
|
133 ./src/Pure/General/xml.scala\\ |
|
134 ./src/Pure/General/linear\_set.scala\\ |
|
135 |
|
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\\ |
|
143 :\\ |
|
144 ./src/Pure/General/sha1.scala\\ |
|
145 ./src/Pure/General/timing.scala\\ |
|
146 ./src/Pure/General/pretty.scala\\ |
|
147 .\\ |
|
148 ./src/Pure/Concurrent/volatile.scala\\ |
|
149 ./src/Pure/Concurrent/future.scala\\ |
|
150 ./src/Pure/Concurrent/simple\_thread.scala\\ |
|
151 .\\ |
|
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\\ |
|
158 .\\ |
|
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\\ |
|
163 .\\ |
|
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\\ |
|
168 .\\ |
|
169 ./src/Pure/Concurrent/volatile.scala\\ |
|
170 ./src/Pure/Concurrent/future.scala\\ |
|
171 ./src/Pure/Concurrent/simple\_thread.scala\\ |
|
172 .\\ |
|
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\\ |
|
179 .\\ |
|
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\\ |
|
184 .\\ |
|
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\\ |
|
197 .\\ |
|
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 |
|
203 } |
|
204 \end{frame} |
|
205 |
|
206 |
|
207 |
|
208 \subsection[jEdit]{Das Frontend: jEdit und ``plugins''} |
|
209 \begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''} |
|
210 \begin{itemize} |
|
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.''} |
|
212 \pause |
|
213 \item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt |
|
214 \pause |
|
215 \item Isabelle verwendet eine Reihe davon |
|
216 \begin{itemize} |
|
217 \item der Parser ``Sidekick'' |
|
218 \item Console f\"ur jEdit-Komponenten |
|
219 \item + Scala |
|
220 \item + Ml |
|
221 \item etc |
|
222 \end{itemize} |
|
223 \pause |
|
224 \item jEdit ist ``open source'' mit gro\3er Community |
|
225 \pause |
|
226 \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle |
|
227 \end{itemize} |
|
228 \end{frame} |
|
229 |
|
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.\\ |
|
234 |
|
235 \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\ |
|
236 |
|
237 Milestones: |
|
238 \begin{enumerate} |
|
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 |
|
243 \begin{itemize} |
|
244 \item jEdit Plugin f\"ur SD |
|
245 \item zugeh\"origen Parser |
|
246 \item nicht vorgesehen: SD-Interpreter in Isar (SML) |
|
247 \end{itemize} |
|
248 \end{enumerate} |
|
249 \end{frame} |
|
250 |
|
251 %\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)} |
|
252 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)} |
|
253 {\footnotesize |
|
254 \begin{tabbing} |
|
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}\}$\\ |
|
270 \> \>$1-x$ |
|
271 \end{tabbing} |
|
272 } |
|
273 \end{frame} |
|
274 |
|
275 \subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE} |
|
276 \begin{frame}\frametitle{Konfiguration in NetBeans} |
|
277 Mehrere Run-Konfigurationen sind praktisch: |
|
278 \begin{itemize} |
|
279 \item Start von jEdit + Plug-ins aus NetBeans |
|
280 \begin{itemize} |
|
281 \item Exekution der fertig kompilierten jEdit.jar |
|
282 \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen ! |
|
283 \end{itemize} |
|
284 \item Start von jEdit aus der Konsole |
|
285 \end{itemize} |
|
286 \vspace{0.2cm} \pause |
|
287 Dementsprechend komplex sind die Konfigurations-Files: |
|
288 \begin{center} |
|
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} |
|
295 \end{center} |
|
296 \end{frame} |
|
297 |
|
298 \subsection[Implementation]{Komponenten zur Implementation von SD} |
|
299 |
|
300 \begin{frame}\frametitle{Die Konzeption des Scala-Layers} |
|
301 \begin{figure} |
|
302 \includegraphics[width=100mm]{fig-jedit-plugins-SD} |
|
303 \label{Frontend des jEdit} |
|
304 \end{figure} |
|
305 \end{frame} |
|
306 |
|
307 \begin{frame}\frametitle{jEdit-Plugin} |
|
308 \begin{itemize} |
|
309 \item Aufbau: Ein Plugin besteht aus: |
|
310 \pause |
|
311 \begin{itemize} |
|
312 \item Source-Files: \textbf{Scala} |
|
313 \pause |
|
314 \item Property file |
|
315 \pause |
|
316 \item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin) |
|
317 \end{itemize} |
|
318 %\pause |
|
319 %\item Bestehendes Java-Plugin in Scala transferieren |
|
320 %\pause |
|
321 %\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren |
|
322 \end{itemize} |
|
323 \end{frame} |
|
324 |
|
325 \begin{frame}\frametitle{Sources des jEdit Plugins} |
|
326 {\tiny |
|
327 src/Tools/jEditC\textbf{\$ ls -l *}\\ |
|
328 build.xml\\ |
|
329 %makedist\\ |
|
330 %manifest.mf\\ |
|
331 %README\_BUILD\\ |
|
332 \textbf{build/*}\\ |
|
333 \textbf{contrib/*}\\ |
|
334 \textbf{dist/*}\\ |
|
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 |
|
365 } |
|
366 \end{frame} |
|
367 |
|
368 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin} |
|
369 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt: |
|
370 \pause |
|
371 \begin{itemize} |
|
372 \item Grunds\"atzlicher Aufbau eines GUIs |
|
373 \pause |
|
374 \item Kopieren von Text zwischen den einzelnen Buffers |
|
375 \pause |
|
376 \begin{itemize} |
|
377 \item \alert{Somit auch Zugriff auf andere Plugins!} |
|
378 \end{itemize} |
|
379 \pause |
|
380 \item Ansatz f\"ur die Einbindung des SD-Parsers |
|
381 \pause |
|
382 \begin{itemize} |
|
383 \item Zugriff auf Isabelle-Pure: \alert{parsen von SD parallel zu Isabelle/Isar} |
|
384 \end{itemize} |
|
385 \pause |
|
386 \item \textit{DEMO} |
|
387 \end{itemize} |
|
388 \end{frame} |
|
389 |
|
390 |
|
391 %\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)} |
|
392 |
|
393 \section[Summary]{Zusammenfassung} |
|
394 \begin{frame}\frametitle{Zusammenfassung} |
|
395 Folgende Milestones wurden erfolgreich abgeschlossen: |
|
396 \begin{enumerate} |
|
397 \item Relevante Isabelle Komponenten dokumentiert |
|
398 \pause |
|
399 \item Installation der Standard-Komponenten: |
|
400 \begin{itemize} |
|
401 \item Mercurial Versioncontrol |
|
402 \item NetBeans IDE |
|
403 \item Standard Isabelle Bundle |
|
404 \end{itemize} |
|
405 \pause |
|
406 \item Entwicklungsumgebung vom Isabelle-Team kopieren |
|
407 \begin{itemize} |
|
408 \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML) |
|
409 \item jEdit als NetBeans Projekt definiert |
|
410 \end{itemize} |
|
411 \pause |
|
412 \item Relevante Komponenten implementieren |
|
413 \begin{itemize} |
|
414 \item jEdit Plugin f\"ur SD |
|
415 \item Verbindung des Plugins zu Isabelle |
|
416 \item zugeh\"origen Parser: nur ein Test in SML |
|
417 \end{itemize} |
|
418 \end{enumerate} |
|
419 \end{frame} |
|
420 |
|
421 \begin{frame}\frametitle{Zusammenfassung} |
|
422 \pause |
|
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.\\ |
|
426 \vspace{0.3cm} |
|
427 \alert{$\mathbf{+ + +}$}\\ |
|
428 \pause |
|
429 Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen: |
|
430 \begin{enumerate} |
|
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). |
|
434 \end{enumerate} |
|
435 \end{frame} |
|
436 |
|
437 \begin{frame}\frametitle{} |
|
438 \begin{center} |
|
439 \LARGE{Danke f\"ur die Aufmerksamkeit !} |
|
440 \end{center} |
|
441 \end{frame} |
|
442 |
|
443 \end{document} |
|
444 |
|
445 |