90 \begin{itemize} |
67 \begin{itemize} |
91 \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots |
68 \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots |
92 \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots |
69 \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots |
93 \item High Order Logics, Logic of Computable Functions, \dots |
70 \item High Order Logics, Logic of Computable Functions, \dots |
94 \end{itemize} |
71 \end{itemize} |
|
72 \pause |
95 \item Math.Grundlagen f\"ur Softwaretechnologie |
73 \item Math.Grundlagen f\"ur Softwaretechnologie |
96 \begin{itemize} |
74 \begin{itemize} |
97 \item Hoare Logic, Temporal Logic of Actions, Hoare for Java |
75 \item Hoare Logic, Temporal Logic of Actions, Hoare for Java |
98 \item Theory for Unix file-system security, for state spaces, \dots |
76 \item Theory for Unix file-system security, for state spaces, \dots |
99 \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net} |
77 \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net} |
100 \end{itemize} |
78 \end{itemize} |
101 \end{itemize} |
79 \end{itemize} |
|
80 \pause |
102 \item Integration von Isabelle in Entwicklungstools |
81 \item Integration von Isabelle in Entwicklungstools |
103 \begin{itemize} |
82 \begin{itemize} |
104 \item Boogie --- Verification Condition Generator |
83 \item Boogie --- Verification Condition Generator |
105 \item ? Test Case Generators (TUG) ? |
84 \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs |
106 \item \dots ??? |
85 \item Test Case Generators (TUG) ? |
107 \end{itemize} |
86 \end{itemize} |
|
87 \pause |
108 \item Isar, die Beweissprache von Isabelle |
88 \item Isar, die Beweissprache von Isabelle |
109 \pause |
|
110 \begin{itemize} |
89 \begin{itemize} |
111 \item Demo |
90 \item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$ |
|
91 \pause |
|
92 \alert{Beweisteile asynchron interpretiert} |
112 \end{itemize} |
93 \end{itemize} |
113 \end{itemize} |
94 \end{itemize} |
114 \end{frame} |
95 \end{frame} |
115 |
96 |
116 \section[Komponenten]{Komponenten des kommenden Isabelle Frontends} |
97 \section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end} |
117 \subsection[Scala]{Scala und ``Actors''} |
98 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers} |
118 \subsection[jEdit]{jEdit und ``Plugins''} |
99 \begin{frame}\frametitle{Die Konzeption des Scala-Layers} |
119 \subsection[Integration]{Integration von Scala und ML} |
100 \begin{figure} |
120 |
101 \begin{center} |
121 \section[NetBeans]{Installation der Komponenten in NetBeans} |
102 \includegraphics[width=75mm]{fig/archi/fig-reuse-ml-scala-SD} |
122 \subsection[TODO]{TODO} |
103 \end{center} |
123 |
104 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.} |
124 \section[NetBeans]{Vorbereitung f\"ur ``structured derivations''} |
105 \label{fig-reuse-ml-scala} |
125 \subsection[Parsen]{Parsen von Isar-Texten} |
106 \end{figure} |
126 |
107 \end{frame} |
127 \section*{Summary} |
108 |
128 \begin{frame} |
109 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML} |
129 \frametitle<presentation>{Summary} |
110 \begin{itemize} |
130 |
111 \item Das Protokoll ist \textbf{asynchron}: \\ |
131 Summary TODO |
112 verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert |
|
113 \pause |
|
114 \item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen) |
|
115 \pause |
|
116 \item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\ |
|
117 \pause |
|
118 Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\ |
|
119 \pause |
|
120 Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\ |
|
121 \pause |
|
122 \alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}} |
|
123 \end{itemize} |
|
124 \end{frame} |
|
125 |
|
126 \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium} |
|
127 \begin{frame}\frametitle{Isabelle Files: *.jar} |
|
128 {\footnotesize |
|
129 ----- for ``isabelle jedit \&''; contained in Isabelle\_bundle}\\ |
|
130 {\tiny |
|
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\\ |
|
146 |
|
147 {\footnotesize |
|
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\\ |
|
163 } |
|
164 \end{frame} |
|
165 |
|
166 \begin{frame}\frametitle{Isabelle Files: *.scala} |
|
167 {\tiny |
|
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\\ |
|
180 .\\ |
|
181 ./src/Pure/Concurrent/volatile.scala\\ |
|
182 ./src/Pure/Concurrent/future.scala\\ |
|
183 ./src/Pure/Concurrent/simple\_thread.scala\\ |
|
184 .\\ |
|
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\\ |
|
191 .\\ |
|
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\\ |
|
196 .\\ |
|
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\\ |
|
209 .\\ |
|
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 |
|
215 } |
|
216 \end{frame} |
|
217 |
|
218 \begin{frame}\frametitle{*.scala --- *.ML} |
|
219 {\footnotesize |
|
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\\ |
|
237 |
|
238 } |
|
239 \end{frame} |
|
240 |
|
241 \subsection[jEdit]{Das Frontend: jEdit und ``plugins''} |
|
242 \begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''} |
|
243 \begin{itemize} |
|
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.''} |
|
245 \pause |
|
246 \item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt |
|
247 \pause |
|
248 \item Isabelle verwendet eine Reihe davon |
|
249 \begin{itemize} |
|
250 \item der Parser ``Sidekick'' |
|
251 \item Console f\"ur jEdit-Komponenten |
|
252 \item + Scala |
|
253 \item + Ml |
|
254 \item etc |
|
255 \end{itemize} |
|
256 \pause |
|
257 \item jEdit ist ``open source'' mit gro\3er Community |
|
258 \pause |
|
259 \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle |
|
260 \end{itemize} |
|
261 \end{frame} |
|
262 |
|
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)} |
|
266 {\footnotesize |
|
267 \begin{tabbing} |
|
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}\}$\\ |
|
283 \> \>$1-x$ |
|
284 \end{tabbing} |
|
285 } |
|
286 \end{frame} |
|
287 |
|
288 \subsection[NetBeans]{Aufsetzen des Projektes in der NetBeans IDE} |
|
289 \subsection[Implementation]{Komponenten zur von SD} |
|
290 \subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)} |
|
291 |
|
292 \section[Summary]{Zusammenfassung} |
|
293 \begin{frame}\frametitle{Zusammenfassung} |
|
294 Zusammenfassung TODO |
|
295 \end{frame} |
|
296 |
|
297 \begin{frame}\frametitle{} |
132 \end{frame} |
298 \end{frame} |
133 |
299 |
134 \end{document} |
300 \end{document} |
135 |
301 |
136 |
302 |