wneuper/isa: doc-src/isac/msteger/bakk-presentation.tex@2b69a774afd5

     1 % /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex

     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}

    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

    22 }

    23 \subtitle{Bachelorarbeit Telematik}

    25 \author{Marco Steger}

    26 \institute{Institut f\"ur Software Technologie\\

    27   Technische Universit\"at Graz}

    29 \date{21.06.2011}

    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:

    35 \AtBeginSubsection[]

    36 {

    37   \begin{frame}<beamer>

    38     \frametitle{Outline}

    39     \tableofcontents[currentsection,currentsubsection]

    40   \end{frame}

    41 }

    44 % If you wish to uncover everything in a step-wise fashion, uncomment

    45 % the following command:

    46 %\beamerdefaultoverlayspecification{<+->}

    49 \begin{document}

    50 \begin{frame}

    51   \titlepage

    52 \end{frame}

    54 \begin{frame}

    55   \frametitle{Outline}

    56   \tableofcontents

    57   % You might wish to add the option [pausesections]

    58 \end{frame}

    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}

    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}

   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}

   127 \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}

   128 <<<<<<< local

   130 =======

   131 >>>>>>> other

   133 <<<<<<< local

   134 %\begin{frame}\frametitle{Isabelle Files: *.jar}

   135 %{\footnotesize

   136 %----- for ``isabelle jedit \&''; contained in Isabelle\_bundle}\\

   137 %{\tiny

   138 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar\\

   139 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar\\

   140 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar\\

   141 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar\\

   142 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \alert{$\;\;\;\;\;\;\;\;\;\;\;\Longleftarrow$ entry to SML}\\

   143 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar\\

   144 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar\\

   145 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar\\

   146 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar\\

   147 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar\\

   148 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar\\

   149 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar\\

   150 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar\\

   151 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar\\

   152 %./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar\\

   153 %

   154 %{\footnotesize

   155 %----- scala system; contained in Isabelle\_bundle}\\

   156 %./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar\\

   157 %./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar\\

   158 %./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar\\

   159 %./contrib/scala-2.8.1.final/lib/scala-compiler.jar\\

   160 %./contrib/scala-2.8.1.final/lib/scalap.jar\\

   161 %./contrib/scala-2.8.1.final/lib/scala-swing.jar\\

   162 %./contrib/scala-2.8.1.final/lib/scala-library.jar\\

   163 %./contrib/scala-2.8.1.final/lib/jline.jar\\

   164 %./contrib/scala-2.8.1.final/lib/scala-dbc.jar\\

   165 %./contrib/scala-2.8.1.final/src/scala-library-src.jar\\

   166 %./contrib/scala-2.8.1.final/src/scala-swing-src.jar\\

   167 %./contrib/scala-2.8.1.final/src/scala-compiler-src.jar\\

   168 %./contrib/scala-2.8.1.final/src/scala-dbc-src.jar\\

   169 %./contrib/scala-2.8.1.final/src/sbaz-src.jar\\

   170 %}

   171 %\end{frame}

   172 %

   173 %\begin{frame}\frametitle{Isabelle Files: *.scala}

   174 %{\tiny

   175 %./src/Pure/General/xml.scala\\

   176 %./src/Pure/General/linear\_set.scala\\

   177 =======

   178 \begin{frame}\frametitle{Isabelle Files: *.scala}

   179 {\tiny

   180 \textbf{\$ find -name ``*.scala''}\\

   181 ./src/Pure/General/xml.scala\\

   182 ./src/Pure/General/linear\_set.scala\\

   183 >>>>>>> other

   184 %./src/Pure/General/symbol.scala\\

   185 %./src/Pure/General/exn.scala\\

   186 %./src/Pure/General/position.scala\\

   187 %./src/Pure/General/scan.scala\\

   188 %./src/Pure/General/xml\_data.scala\\

   189 %./src/Pure/General/yxml.scala\\

   190 %./src/Pure/General/markup.scala\\

   191 <<<<<<< local

   192 =======

   193 :\\

   194 >>>>>>> other

   195 %./src/Pure/General/sha1.scala\\

   196 <<<<<<< local

   197 %./src/Pure/General/timing.scala\\

   198 %./src/Pure/General/pretty.scala\\

   199 %.\\

   200 %./src/Pure/Concurrent/volatile.scala\\

   201 %./src/Pure/Concurrent/future.scala\\

   202 %./src/Pure/Concurrent/simple\_thread.scala\\

   203 %.\\

   204 %./src/Pure/Thy/html.scala\\

   205 %./src/Pure/Thy/completion.scala\\

   206 %./src/Pure/Thy/thy\_header.scala\\

   207 %./src/Pure/Thy/thy\_syntax.scala\\

   208 %./src/Pure/Isac/isac.scala\\

   209 %./src/Pure/library.scala\\

   210 %.\\

   211 %./src/Pure/Isar/keyword.scala\\

   212 %./src/Pure/Isar/outer\_syntax.scala\\

   213 %./src/Pure/Isar/token.scala\\

   214 %./src/Pure/Isar/parse.scala\\

   215 %.\\

   216 %./src/Pure/System/gui\_setup.scala\\

   217 %./src/Pure/System/isabelle\_system.scala\\

   218 =======

   219 ./src/Pure/General/timing.scala\\

   220 ./src/Pure/General/pretty.scala\\

   221 .\\

   222 ./src/Pure/Concurrent/volatile.scala\\

   223 ./src/Pure/Concurrent/future.scala\\

   224 ./src/Pure/Concurrent/simple\_thread.scala\\

   225 .\\

   226 ./src/Pure/Thy/html.scala\\

   227 ./src/Pure/Thy/completion.scala\\

   228 ./src/Pure/Thy/thy\_header.scala\\

   229 ./src/Pure/Thy/thy\_syntax.scala\\

   230 ./src/Pure/Isac/isac.scala\\

   231 ./src/Pure/library.scala\\

   232 .\\

   233 ./src/Pure/Isar/keyword.scala\\

   234 ./src/Pure/Isar/outer\_syntax.scala\\

   235 ./src/Pure/Isar/token.scala\\

   236 ./src/Pure/Isar/parse.scala\\

   237 .\\

   238 ./src/Pure/System/gui\_setup.scala\\

   239 ./src/Pure/System/isabelle\_system.scala\\

   240 >>>>>>> other

   241 %./src/Pure/System/swing\_thread.scala\\

   242 %./src/Pure/System/download.scala\\

   243 %./src/Pure/System/session\_manager.scala\\

   244 %./src/Pure/System/standard\_system.scala\\

   245 %./src/Pure/System/isabelle\_syntax.scala\\

   246 %./src/Pure/System/session.scala\\

   247 %./src/Pure/System/platform.scala\\

   248 %./src/Pure/System/cygwin.scala\\

   249 <<<<<<< local

   250 %./src/Pure/System/event\_bus.scala\\

   251 %./src/Pure/System/isabelle\_process.scala\\

   252 %.\\

   253 %./src/Pure/PIDE/document.scala\\

   254 %./src/Pure/PIDE/markup\_tree.scala\\

   255 %./src/Pure/PIDE/text.scala\\

   256 %./src/Pure/PIDE/command.scala\\

   257 %./src/Pure/PIDE/isar\_document.scala

   258 %}

   259 %\end{frame}

   260 =======

   261 :\\

   262 ./src/Pure/System/event\_bus.scala\\

   263 ./src/Pure/System/isabelle\_process.scala\\

   264 .\\

   265 ./src/Pure/PIDE/document.scala\\

   266 ./src/Pure/PIDE/markup\_tree.scala\\

   267 ./src/Pure/PIDE/text.scala\\

   268 ./src/Pure/PIDE/command.scala\\

   269 ./src/Pure/PIDE/isar\_document.scala

   270 }

   271 \end{frame}

   272 >>>>>>> other

   274 \begin{frame}\frametitle{*.scala --- *.ML}

   275 {\footnotesize

   276 isabisac\$ ls -l src/Pure/System/\\

   277 -rw-r--r-- 1 msteger root  3987 2011-03-14 17:09 cygwin.scala\\

   278 -rw-r--r-- 1 msteger root  1486 2011-03-14 17:09 download.scala\\

   279 -rw-r--r-- 1 msteger root  1296 2011-03-14 17:09 event\_bus.scala\\

   280 -rw-r--r-- 1 msteger root  1830 2011-03-14 17:09 gui\_setup.scala\\

   281 -rw-r--r-- 1 msteger root  5722 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{ML}\\

   282 -rw-r--r-- 1 msteger root 1059 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{scala}\\

   283 -rw-r--r-- 1 msteger root  1659 2011-03-14 17:09 isabelle\_syntax.scala\\

   284 -rw-r--r-- 1 msteger root  2087 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{ML}\\

   285 -rw-r--r-- 1 msteger root 1168 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{scala}\\

   286 -rw-r--r-- 1 msteger root  5935 2011-03-14 17:09 isar.ML\\

   287 -rw-r--r-- 1 msteger root  1989 2011-03-14 17:09 platform.scala\\

   288 -rw-r--r-- 1 msteger root  1427 2011-03-14 17:09 session\_manager.scala\\

   289 -rw-r--r-- 1 msteger root  3833 2011-03-14 17:09 \alert{session}.\textbf{ML}\\

   290 -rw-r--r-- 1 msteger root  9172 2011-03-14 17:09 \alert{session}.\textbf{scala}\\

   291 -rw-r--r-- 1 msteger root  9086 2011-03-14 17:09 standard\_system.scala\\

   292 -rw-r--r-- 1 msteger root  1643 2011-03-14 17:09 swing\_thread.scala\\

   294 }

   295 \end{frame}

   297 \subsection[jEdit]{Das Frontend: jEdit und ``plugins''}

   298 \begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''}

   299 \begin{itemize}

   300 \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.''}

   301 \pause

   302 \item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt

   303 \pause

   304 \item Isabelle verwendet eine Reihe davon

   305   \begin{itemize}

   306   \item der Parser ``Sidekick''

   307   \item Console f\"ur jEdit-Komponenten

   308   \item + Scala

   309   \item + Ml

   310   \item etc

   311   \end{itemize}

   312 \pause

   313 \item jEdit ist ``open source'' mit gro\3er Community

   314 \pause

   315 \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle

   316 \end{itemize}

   317 \end{frame}

   319 \section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)}

   320 \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}

   321 \begin{frame}\frametitle{Definition der Aufgabenstellung}

   322 Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured~derivations'' (SD) in Isabelle.\\

   324 \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\

   326 Milestones:

   327 \begin{enumerate}

   328 \item Relevante Isabelle Komponenten identifizieren und studieren

   329 \item Installation der Standard-Komponenten

   330 \item Entwicklungsumgebung vom Isabelle-Team kopieren

   331 \item Relevante Komponenten implementieren

   332   \begin{itemize}

   333   \item jEdit Plugin f\"ur SD

   334   \item zugeh\"origen Parser

   335   \item nicht vorgesehen: SD-Interpreter in Isar (SML)

   336   \end{itemize}

   337 \end{enumerate}

   338 \end{frame}

   340 %\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}

   341 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}

   342 {\footnotesize

   343 \begin{tabbing}

   344 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill

   345 \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\

   346 \>  \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\

   347 \>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\

   348 \>  \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\

   349 \>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\

   350 \>  \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\

   351 \>  \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\

   352 \>  \>   \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\

   353 \>  \>$\equiv$\>\vdots\\

   354 \>  \>  \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\

   355 \>  \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$  \\

   356 \>  \>     \>$1 + -1 * x$\\

   357 \>\dots\>$1 + -1 * x$\\

   358 \>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\

   359 \>  \>$1-x$

   360 \end{tabbing}

   361 }

   362 \end{frame}

   364 \subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE}

   365 \begin{frame}\frametitle{Konfiguration in NetBeans}

   366 Mehrere Run-Konfigurationen sind praktisch:

   367 \begin{itemize}

   368 \item Start von jEdit + Plug-ins aus NetBeans

   369   \begin{itemize}

   370   \item Exekution der fertig kompilierten jEdit.jar

   371   \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen !

   372   \end{itemize}

   373 \item Start von jEdit aus der Konsole

   374 \end{itemize}

   375 \vspace{0.2cm}   \pause

   376 Dementsprechend komplex sind die Konfigurations-Files:

   377 \begin{center}

   378 \begin{tabular}{l r l}

   379 build.xml          & 102 & LOCs\\

   380 project.xml        & 25  & LOCs\\

   381 project.properties & 85  & LOCs\\

   382 build-impl.xml     & 708 & LOCs\\

   383                    &     & (teilw. automatisch generiert)\end{tabular}

   384 \end{center}

   385 \end{frame}

   387 \subsection[Implementation]{Komponenten zur Implementation von SD}

   389 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}

   390 \begin{figure}

   391 \includegraphics[width=100mm]{fig-jedit-plugins-SD}

   392 \label{Frontend des jEdit}

   393 \end{figure}

   394 \end{frame}

   396 \begin{frame}\frametitle{jEdit-Plugin}

   397 \begin{itemize}

   398 \item Aufbau: Ein Plugin besteht aus:

   399 \pause

   400 	\begin{itemize}

   401 	\item Source-Files: \textbf{Scala}

   402 	\pause

   403 	\item Property file

   404 	\pause

   405 	\item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)

   406 	\end{itemize}

   407 %\pause

   408 %\item Bestehendes Java-Plugin in Scala transferieren

   409 %\pause

   410 %\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren

   411 \end{itemize}

   412 \end{frame}

   414 \begin{frame}\frametitle{Sources des jEdit Plugins}

   415 {\tiny

   416 src/Tools/jEditC\textbf{\$ ls -l *}\\

   417 build.xml\\

   418 %makedist\\

   419 %manifest.mf\\

   420 %README\_BUILD\\

   421 \textbf{build/*}\\

   422 \textbf{contrib/*}\\

   423 \textbf{dist/*}\\

   424 \textbf{plugin/}build.xml\\

   425 \textbf{plugin/}changes40.txt\\

   426 \textbf{plugin/}changes42.txt\\

   427 \textbf{plugin/}description.html\\

   428 \textbf{plugin/}IsacActions.java\\

   429 \textbf{plugin/}Isac.iml\\

   430 \textbf{plugin/}Isac.java\\

   431 \textbf{plugin/}IsacOptionPane.java\\

   432 \textbf{plugin/}IsacPlugin.java\\

   433 \textbf{plugin/}IsacTextArea.java\\

   434 \textbf{plugin/}IsacToolPanel.java\\

   435 \textbf{plugin/}plugin\\

   436 \textbf{plugin/}README.txt\\

   437 \textbf{nbproject/*}\\

   438 \textbf{src/}actions.xml\\

   439 \textbf{src/}changes40.txt\\

   440 \textbf{src/}changes42.txt\\

   441 \textbf{src/}description.html\\

   442 \textbf{src/}dockables.xml\\

   443 \textbf{src/}IsacActions.scala\\

   444 \textbf{src/}Isac.iml\\

   445 \textbf{src/}IsacOptionPane.scala\\

   446 \textbf{src/}IsacPlugin.scala\\

   447 \textbf{src/}Isac.props\\

   448 \textbf{src/}Isac.scala\\

   449 \textbf{src/}IsacTextArea.scala\\

   450 \textbf{src/}IsacToolPanel.scala\\

   451 \textbf{src/}manifest.mf\\

   452 \textbf{src/}README.txt\\

   453 \textbf{src/}users-guide.xml

   454 }

   455 \end{frame}

   457 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}

   458 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:

   459 \pause

   460 \begin{itemize}

   461 	\item Grunds\"atzlicher Aufbau eines GUIs

   462 	\pause

   463 	\item Kopieren von Text zwischen den einzelnen Buffers

   464 	\pause

   465 		\begin{itemize}

   466 		\item \alert{Somit auch Zugriff auf andere Plugins!}

   467 		\end{itemize}

   468 	\pause

   469 	\item Ansatz f\"ur die Einbindung des SD-Parsers

   470 	\pause

   471 		\begin{itemize}

   472 		\item Zugriff auf Isabelle-Pure: \alert{parsen von SD parallel zu Isabelle/Isar}

   473 		\end{itemize}

   474 	\pause

   475 	\item \textit{DEMO}

   476 \end{itemize}

   477 \end{frame}

   480 %\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}

   482 \section[Summary]{Zusammenfassung}

   483 \begin{frame}\frametitle{Zusammenfassung}

   484 Folgende Milestones wurden erfolgreich abgeschlossen:

   485 \begin{enumerate}

   486 \item Relevante Isabelle Komponenten dokumentiert

   487 \pause

   488 \item Installation der Standard-Komponenten:

   489   \begin{itemize}

   490   \item Mercurial Versioncontrol

   491   \item NetBeans IDE

   492   \item Standard Isabelle Bundle

   493   \end{itemize}

   494   \pause

   495 \item Entwicklungsumgebung vom Isabelle-Team kopieren

   496   \begin{itemize}

   497   \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)

   498   \item jEdit als NetBeans Projekt definiert

   499   \end{itemize}

   500   \pause

   501 \item Relevante Komponenten implementieren

   502   \begin{itemize}

   503   \item jEdit Plugin f\"ur SD

   504   \item Verbindung des Plugins zu Isabelle

   505   \item zugeh\"origen Parser: nur ein Test in SML

   506   \end{itemize}

   507 \end{enumerate}

   508 \end{frame}

   510 \begin{frame}\frametitle{Zusammenfassung}

   511 \pause

   512 \alert{$\mathbf{- - -}$}\\

   513 Aus Zeitgr\"unden nicht m\"oglich: ein komplettes SD-Plugin;\\

   514 dazu w\"are auch ein Interpreter auf der ML-Seite n\"otig.\\

   515 \vspace{0.3cm}

   516 \alert{$\mathbf{+ + +}$}\\

   517 \pause

   518 Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen:

   519 \begin{enumerate}

   520 \item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots

   521 \item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend

   522 \item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).

   523 \end{enumerate}

   524 \end{frame}

   526 \begin{frame}\frametitle{}

   527 \begin{center}

   528 \LARGE{Danke f\"ur die Aufmerksamkeit !}

   529 \end{center}

   530 \end{frame}

   532 \end{document}

author	Marco Steger <m.steger@student.tugraz.at>
	Wed, 22 Jun 2011 19:48:14 +0200
branch	decompose-isar
changeset 42050	2b69a774afd5
parent 42048	6548da70f14e
child 42052	39d3f1dfbece
permissions	-rw-r--r--