92 \alert{Beweisteile asynchron interpretiert} |
93 \alert{Beweisteile asynchron interpretiert} |
93 \end{itemize} |
94 \end{itemize} |
94 \end{itemize} |
95 \end{itemize} |
95 \end{frame} |
96 \end{frame} |
96 |
97 |
97 \section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end} |
|
98 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers} |
98 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers} |
99 \begin{frame}\frametitle{Die Konzeption des Scala-Layers} |
99 \begin{frame}\frametitle{Die Konzeption des Scala-Layers} |
100 %\begin{figure} |
100 \begin{figure} |
101 %\begin{center} |
101 \begin{center} |
102 %\includegraphics[width=75mm]{fig/archi/fig-reuse-ml-scala-SD} |
102 \includegraphics[width=100mm]{fig-reuse-ml-scala-SD} |
103 %\end{center} |
103 \end{center} |
104 %%\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.} |
104 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.} |
105 %\label{fig-reuse-ml-scala} |
105 \label{fig-reuse-ml-scala} |
106 %\end{figure} |
106 \end{figure} |
107 \end{frame} |
107 \end{frame} |
108 |
108 |
109 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML} |
109 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML} |
110 \begin{itemize} |
110 \begin{itemize} |
111 \item Das Protokoll ist \textbf{asynchron}: \\ |
111 \item Das Protokoll ist \textbf{asynchron}: \\ |
258 \pause |
258 \pause |
259 \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle |
259 \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle |
260 \end{itemize} |
260 \end{itemize} |
261 \end{frame} |
261 \end{frame} |
262 |
262 |
263 \section[Projektarbeit]{Projektarbeit: Vorbereitungen f\"ur ``structured derivations''} |
263 \section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)} |
264 \subsection[Beispiel SD]{Beispiel ``structured derivation'' (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.\\ |
|
267 |
|
268 \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\ |
|
269 |
|
270 Milestones: |
|
271 \begin{enumerate} |
|
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 |
|
276 \begin{itemize} |
|
277 \item jEdit Plugin f\"ur SD |
|
278 \item zugeh\"origen Parser |
|
279 \item nicht vorgesehen: SD-Interpreter in Isar (SML) |
|
280 \end{itemize} |
|
281 \end{enumerate} |
|
282 \end{frame} |
|
283 |
|
284 %\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)} |
265 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)} |
285 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)} |
266 {\footnotesize |
286 {\footnotesize |
267 \begin{tabbing} |
287 \begin{tabbing} |
268 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill |
288 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill |
269 \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\ |
289 \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\ |
283 \> \>$1-x$ |
303 \> \>$1-x$ |
284 \end{tabbing} |
304 \end{tabbing} |
285 } |
305 } |
286 \end{frame} |
306 \end{frame} |
287 |
307 |
288 \subsection[NetBeans]{Aufsetzen des Projektes in der NetBeans IDE} |
308 \subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE} |
289 \begin{frame}\frametitle{Grundlegender Aufbau eines jEdit-Plugin} |
309 \begin{frame}\frametitle{Konfiguration in NetBeans} |
290 \begin{itemize} |
310 Mehrere Run-Konfigurationen sind praktisch: |
291 \item Ein Plugin besteht aus: |
311 \begin{itemize} |
|
312 \item Start von jEdit + Plug-ins aus NetBeans |
|
313 \begin{itemize} |
|
314 \item Exekution der fertig kompilierten jEdit.jar |
|
315 \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen ! |
|
316 \end{itemize} |
|
317 \item Start von jEdit aus der Konsole |
|
318 \end{itemize} |
|
319 \vspace{0.2cm} \pause |
|
320 Dementsprechend komplex sind die Konfigurations-Files: |
|
321 \begin{center} |
|
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} |
|
328 \end{center} |
|
329 \end{frame} |
|
330 |
|
331 \subsection[Implementation]{Komponenten zur Implementation von SD} |
|
332 |
|
333 \begin{frame}\frametitle{Die Konzeption des Scala-Layers} |
|
334 \begin{figure} |
|
335 \includegraphics[width=100mm]{fig-jedit-plugins-SD} |
|
336 \label{Frontend des jEdit} |
|
337 \end{figure} |
|
338 \end{frame} |
|
339 |
|
340 \begin{frame}\frametitle{jEdit-Plugin} |
|
341 \begin{itemize} |
|
342 \item Aufbau: Ein Plugin besteht aus: |
292 \pause |
343 \pause |
293 \begin{itemize} |
344 \begin{itemize} |
294 \item Source-Files: \textbf{Scala} |
345 \item Source-Files: \textbf{Scala} |
295 \pause |
346 \pause |
296 \item Property file |
347 \item Property file |
297 \pause |
348 \pause |
298 \item XML-Files: \textit{Klebstoff} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin) |
349 \item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin) |
299 \end{itemize} |
350 \end{itemize} |
300 \pause |
351 %\pause |
301 \item Bestehendes Java-Plugin in Scala transferieren |
352 %\item Bestehendes Java-Plugin in Scala transferieren |
302 \pause |
353 %\pause |
303 \item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren |
354 %\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren |
304 \end{itemize} |
355 \end{itemize} |
305 \end{frame} |
|
306 |
|
307 \begin{frame}\frametitle{Die Konzeption des Scala-Layers} |
|
308 \begin{figure} |
|
309 \begin{center} |
|
310 \includegraphics[width=75mm]{fig/block-frontend} |
|
311 \end{center} |
|
312 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.} |
|
313 \label{Frontend des jEdit} |
|
314 \end{figure} |
|
315 \end{frame} |
356 \end{frame} |
316 |
357 |
317 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin} |
358 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin} |
318 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt: |
359 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt: |
319 \pause |
360 \pause |
320 \begin{itemize} |
361 \begin{itemize} |
321 \item Grunds\"atzlicher Aufbau eines GUIs |
362 \item Grunds\"atzlicher Aufbau eines GUIs |
322 \pause |
363 \pause |
323 \item Kopieren von Text zwischen den einzelnen Buffern |
364 \item Kopieren von Text zwischen den einzelnen Buffers |
324 \pause |
365 \pause |
325 \begin{itemize} |
366 \begin{itemize} |
326 \item \alert{Somit auch Zugriff auf andere Plugins!} |
367 \item \alert{Somit auch Zugriff auf andere Plugins!} |
327 \end{itemize} |
368 \end{itemize} |
328 \pause |
369 \pause |
334 \pause |
375 \pause |
335 \item \textit{DEMO} |
376 \item \textit{DEMO} |
336 \end{itemize} |
377 \end{itemize} |
337 \end{frame} |
378 \end{frame} |
338 |
379 |
339 \subsection[Implementation]{Komponenten zur von SD} |
380 |
340 \subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)} |
381 \subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)} |
341 |
382 |
342 \section[Summary]{Zusammenfassung} |
383 \section[Summary]{Zusammenfassung} |
343 \begin{frame}\frametitle{Zusammenfassung} |
384 \begin{frame}\frametitle{Zusammenfassung} |
344 Zusammenfassung TODO |
385 Folgende Milestones wurden erfolgreich abgeschlossen: |
|
386 \begin{enumerate} |
|
387 \item Relevante Isabelle Komponenten dokumentiert (...Std.) |
|
388 \item Installation der Standard-Komponenten: |
|
389 \begin{itemize} |
|
390 \item Mercurial Versioncontrol |
|
391 \item NetBeans IDE |
|
392 \item Standard Isabelle Bundle |
|
393 \end{itemize} |
|
394 \item Entwicklungsumgebung vom Isabelle-Team kopieren |
|
395 \begin{itemize} |
|
396 \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML) |
|
397 \item jEdit als NetBeans Projekt definiert |
|
398 \end{itemize} |
|
399 \item Relevante Komponenten implementieren |
|
400 \begin{itemize} |
|
401 \item jEdit Plugin f\"ur SD |
|
402 \item Verbindung des Plugins zu Isabelle |
|
403 \item zugeh\"origen Parser: nur ein Test in SML |
|
404 \end{itemize} |
|
405 \end{enumerate} |
|
406 \end{frame} |
|
407 |
|
408 \begin{frame}\frametitle{Zusammenfassung} |
|
409 \pause |
|
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.\\ |
|
413 \vspace{0.3cm} |
|
414 \alert{$\mathbf{+ + +}$}\\ |
|
415 Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen: |
|
416 \begin{enumerate} |
|
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). |
|
420 \end{enumerate} |
345 \end{frame} |
421 \end{frame} |
346 |
422 |
347 \begin{frame}\frametitle{} |
423 \begin{frame}\frametitle{} |
|
424 \begin{center} |
|
425 \LARGE{Danke f\"ur die Aufmerksamkeit !} |
|
426 \end{center} |
348 \end{frame} |
427 \end{frame} |
349 |
428 |
350 \end{document} |
429 \end{document} |
351 |
430 |
352 |
431 |