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

     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

   129 <<<<<<< local

   130 <<<<<<< local

   131 =======

   132 >>>>>>> other

   133 =======

   134 >>>>>>> other

   136 <<<<<<< local

   137 <<<<<<< local

   138 =======

   139 >>>>>>> other

   140 =======

   141 >>>>>>> other

   142 =======

   143 >>>>>>> other

   145 <<<<<<< local

   146 <<<<<<< local

   147 <<<<<<< local

   148 =======

   149 >>>>>>> other

   150 =======

   151 >>>>>>> other

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

   153 %{\footnotesize

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

   155 %{\tiny

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   171 %

   172 %{\footnotesize

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   188 %}

   189 %\end{frame}

   190 %

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

   192 %{\tiny

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

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

   195 <<<<<<< local

   196 <<<<<<< local

   197 =======

   198 >>>>>>> other

   199 =======

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

   201 {\tiny

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

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

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

   205 >>>>>>> other

   206 <<<<<<< local

   207 =======

   208 >>>>>>> other

   209 =======

   210 >>>>>>> other

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

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

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

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

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

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

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

   218 <<<<<<< local

   219 <<<<<<< local

   220 =======

   221 >>>>>>> other

   222 <<<<<<< local

   223 =======

   224 :\\

   225 >>>>>>> other

   226 <<<<<<< local

   227 =======

   228 >>>>>>> other

   229 =======

   230 >>>>>>> other

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

   232 <<<<<<< local

   233 <<<<<<< local

   234 <<<<<<< local

   235 =======

   236 >>>>>>> other

   237 =======

   238 >>>>>>> other

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

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

   241 %.\\

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

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

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

   245 %.\\

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

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

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

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

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

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

   252 %.\\

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

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

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

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

   257 %.\\

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

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

   260 <<<<<<< local

   261 <<<<<<< local

   262 =======

   263 >>>>>>> other

   264 =======

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

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

   267 .\\

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

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

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

   271 .\\

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

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

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

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

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

   277 ./src/Pure/library.scala\\

   278 .\\

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

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

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

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

   283 .\\

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

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

   286 >>>>>>> other

   287 <<<<<<< local

   288 =======

   289 >>>>>>> other

   290 =======

   291 >>>>>>> other

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

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

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

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

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

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

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

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

   300 <<<<<<< local

   301 <<<<<<< local

   302 <<<<<<< local

   303 =======

   304 >>>>>>> other

   305 =======

   306 >>>>>>> other

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

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

   309 %.\\

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

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

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

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

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

   315 %}

   316 %\end{frame}

   317 <<<<<<< local

   318 <<<<<<< local

   319 =======

   320 >>>>>>> other

   321 =======

   322 :\\

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

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

   325 .\\

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

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

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

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

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

   331 }

   332 \end{frame}

   333 >>>>>>> other

   334 <<<<<<< local

   335 =======

   336 >>>>>>> other

   337 =======

   338 >>>>>>> other

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

   341 {\footnotesize

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   360 }

   361 \end{frame}

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

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

   365 \begin{itemize}

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

   367 \pause

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

   369 \pause

   370 \item Isabelle verwendet eine Reihe davon

   371   \begin{itemize}

   372   \item der Parser ``Sidekick''

   373   \item Console f\"ur jEdit-Komponenten

   374   \item + Scala

   375   \item + Ml

   376   \item etc

   377   \end{itemize}

   378 \pause

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

   380 \pause

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

   382 \end{itemize}

   383 \end{frame}

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

   386 \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}

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

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

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

   392 Milestones:

   393 \begin{enumerate}

   394 \item Relevante Isabelle Komponenten identifizieren und studieren

   395 \item Installation der Standard-Komponenten

   396 \item Entwicklungsumgebung vom Isabelle-Team kopieren

   397 \item Relevante Komponenten implementieren

   398   \begin{itemize}

   399   \item jEdit Plugin f\"ur SD

   400   \item zugeh\"origen Parser

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

   402   \end{itemize}

   403 \end{enumerate}

   404 \end{frame}

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

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

   408 {\footnotesize

   409 \begin{tabbing}

   410 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill

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

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

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

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

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

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

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

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

   419 \>  \>$\equiv$\>\vdots\\

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

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

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

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

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

   425 \>  \>$1-x$

   426 \end{tabbing}

   427 }

   428 \end{frame}

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

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

   432 Mehrere Run-Konfigurationen sind praktisch:

   433 \begin{itemize}

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

   435   \begin{itemize}

   436   \item Exekution der fertig kompilierten jEdit.jar

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

   438   \end{itemize}

   439 \item Start von jEdit aus der Konsole

   440 \end{itemize}

   441 \vspace{0.2cm}   \pause

   442 Dementsprechend komplex sind die Konfigurations-Files:

   443 \begin{center}

   444 \begin{tabular}{l r l}

   445 build.xml          & 102 & LOCs\\

   446 project.xml        & 25  & LOCs\\

   447 project.properties & 85  & LOCs\\

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

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

   450 \end{center}

   451 \end{frame}

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

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

   456 \begin{figure}

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

   458 \label{Frontend des jEdit}

   459 \end{figure}

   460 \end{frame}

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

   463 \begin{itemize}

   464 \item Aufbau: Ein Plugin besteht aus:

   465 \pause

   466 	\begin{itemize}

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

   468 	\pause

   469 	\item Property file

   470 	\pause

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

   472 	\end{itemize}

   473 %\pause

   474 %\item Bestehendes Java-Plugin in Scala transferieren

   475 %\pause

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

   477 \end{itemize}

   478 \end{frame}

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

   481 {\tiny

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

   483 build.xml\\

   484 %makedist\\

   485 %manifest.mf\\

   486 %README\_BUILD\\

   487 \textbf{build/*}\\

   488 \textbf{contrib/*}\\

   489 \textbf{dist/*}\\

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

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

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

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

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

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

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

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

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

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

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

   501 \textbf{plugin/}plugin\\

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

   503 \textbf{nbproject/*}\\

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   520 }

   521 \end{frame}

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

   524 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:

   525 \pause

   526 \begin{itemize}

   527 	\item Grunds\"atzlicher Aufbau eines GUIs

   528 	\pause

   529 	\item Kopieren von Text zwischen den einzelnen Buffers

   530 	\pause

   531 		\begin{itemize}

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

   533 		\end{itemize}

   534 	\pause

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

   536 	\pause

   537 		\begin{itemize}

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

   539 		\end{itemize}

   540 	\pause

   541 	\item \textit{DEMO}

   542 \end{itemize}

   543 \end{frame}

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

   548 \section[Summary]{Zusammenfassung}

   549 \begin{frame}\frametitle{Zusammenfassung}

   550 Folgende Milestones wurden erfolgreich abgeschlossen:

   551 \begin{enumerate}

   552 \item Relevante Isabelle Komponenten dokumentiert

   553 \pause

   554 \item Installation der Standard-Komponenten:

   555   \begin{itemize}

   556   \item Mercurial Versioncontrol

   557   \item NetBeans IDE

   558   \item Standard Isabelle Bundle

   559   \end{itemize}

   560   \pause

   561 \item Entwicklungsumgebung vom Isabelle-Team kopieren

   562   \begin{itemize}

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

   564   \item jEdit als NetBeans Projekt definiert

   565   \end{itemize}

   566   \pause

   567 \item Relevante Komponenten implementieren

   568   \begin{itemize}

   569   \item jEdit Plugin f\"ur SD

   570   \item Verbindung des Plugins zu Isabelle

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

   572   \end{itemize}

   573 \end{enumerate}

   574 \end{frame}

   576 \begin{frame}\frametitle{Zusammenfassung}

   577 \pause

   578 \alert{$\mathbf{- - -}$}\\

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

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

   581 \vspace{0.3cm}

   582 \alert{$\mathbf{+ + +}$}\\

   583 \pause

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

   585 \begin{enumerate}

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

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

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

   589 \end{enumerate}

   590 \end{frame}

   592 \begin{frame}\frametitle{}

   593 \begin{center}

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

   595 \end{center}

   596 \end{frame}

   598 \end{document}

author	Marco Steger <m.steger@student.tugraz.at>
	Wed, 22 Jun 2011 19:58:58 +0200
branch	decompose-isar
changeset 42053	c455cdfc9f4a
parent 42052	39d3f1dfbece
child 42054	cab075e12fd9
permissions	-rw-r--r--