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

     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{TODO}

    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 \pause

    93 \alert{Beweisteile asynchron interpretiert}

    94   \end{itemize}

    95 \end{itemize}

    96 \end{frame}

    98 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers}

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

   100 \begin{figure}

   101 \begin{center}

   102 \includegraphics[width=100mm]{fig-reuse-ml-scala-SD}

   103 \end{center}

   104 %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}

   105 \label{fig-reuse-ml-scala}

   106 \end{figure}

   107 \end{frame}

   109 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML}

   110 \begin{itemize}

   111 \item Das Protokoll ist \textbf{asynchron}: \\

   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}

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

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

   129 {\tiny

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

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

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

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

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

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

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

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

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

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

   140 :\\

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

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

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

   144 .\\

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

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

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

   148 .\\

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

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

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

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

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

   154 ./src/Pure/library.scala\\

   155 .\\

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

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

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

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

   160 .\\

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

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

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

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

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

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

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

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

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

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

   171 :\\

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

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

   174 .\\

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

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

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

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

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

   180 }

   181 \end{frame}

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

   184 {\footnotesize

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   203 }

   204 \end{frame}

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

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

   208 \begin{itemize}

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

   210 \pause

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

   212 \pause

   213 \item Isabelle verwendet eine Reihe davon

   214   \begin{itemize}

   215   \item der Parser ``Sidekick''

   216   \item Console f\"ur jEdit-Komponenten

   217   \item + Scala

   218   \item + Ml

   219   \item etc

   220   \end{itemize}

   221 \pause

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

   223 \pause

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

   225 \end{itemize}

   226 \end{frame}

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

   229 \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}

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

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

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

   235 Milestones:

   236 \begin{enumerate}

   237 \item Relevante Isabelle Komponenten identifizieren und studieren

   238 \item Installation der Standard-Komponenten

   239 \item Entwicklungsumgebung vom Isabelle-Team kopieren

   240 \item Relevante Komponenten implementieren

   241   \begin{itemize}

   242   \item jEdit Plugin f\"ur SD

   243   \item zugeh\"origen Parser

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

   245   \end{itemize}

   246 \end{enumerate}

   247 \end{frame}

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

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

   251 {\footnotesize

   252 \begin{tabbing}

   253 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill

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

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

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

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

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

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

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

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

   262 \>  \>$\equiv$\>\vdots\\

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

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

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

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

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

   268 \>  \>$1-x$

   269 \end{tabbing}

   270 }

   271 \end{frame}

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

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

   275 Mehrere Run-Konfigurationen sind praktisch:

   276 \begin{itemize}

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

   278   \begin{itemize}

   279   \item Exekution der fertig kompilierten jEdit.jar

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

   281   \end{itemize}

   282 \item Start von jEdit aus der Konsole

   283 \end{itemize}

   284 \vspace{0.2cm}   \pause

   285 Dementsprechend komplex sind die Konfigurations-Files:

   286 \begin{center}

   287 \begin{tabular}{l r l}

   288 build.xml          & 102 & LOCs\\

   289 project.xml        & 25  & LOCs\\

   290 project.properties & 85  & LOCs\\

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

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

   293 \end{center}

   294 \end{frame}

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

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

   299 \begin{figure}

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

   301 \label{Frontend des jEdit}

   302 \end{figure}

   303 \end{frame}

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

   306 \begin{itemize}

   307 \item Aufbau: Ein Plugin besteht aus:

   308 \pause

   309 	\begin{itemize}

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

   311 	\pause

   312 	\item Property file

   313 	\pause

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

   315 	\end{itemize}

   316 %\pause

   317 %\item Bestehendes Java-Plugin in Scala transferieren

   318 %\pause

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

   320 \end{itemize}

   321 \end{frame}

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

   324 {\tiny

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

   326 build.xml\\

   327 %makedist\\

   328 %manifest.mf\\

   329 %README\_BUILD\\

   330 \textbf{build/*}\\

   331 \textbf{contrib/*}\\

   332 \textbf{dist/*}\\

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

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

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

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

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

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

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

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

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

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

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

   344 \textbf{plugin/}plugin\\

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

   346 \textbf{nbproject/*}\\

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   363 }

   364 \end{frame}

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

   367 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:

   368 \pause

   369 \begin{itemize}

   370 	\item Grunds\"atzlicher Aufbau eines GUIs

   371 	\pause

   372 	\item Kopieren von Text zwischen den einzelnen Buffers

   373 	\pause

   374 		\begin{itemize}

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

   376 		\end{itemize}

   377 	\pause

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

   379 	\pause

   380 		\begin{itemize}

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

   382 		\end{itemize}

   383 	\pause

   384 	\item \textit{DEMO}

   385 \end{itemize}

   386 \end{frame}

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

   391 \section[Summary]{Zusammenfassung}

   392 \begin{frame}\frametitle{Zusammenfassung}

   393 Folgende Milestones wurden erfolgreich abgeschlossen:

   394 \begin{enumerate}

   395 \item Relevante Isabelle Komponenten dokumentiert (...Std.)

   396 \item Installation der Standard-Komponenten:

   397   \begin{itemize}

   398   \item Mercurial Versioncontrol

   399   \item NetBeans IDE

   400   \item Standard Isabelle Bundle

   401   \end{itemize}

   402 \item Entwicklungsumgebung vom Isabelle-Team kopieren

   403   \begin{itemize}

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

   405   \item jEdit als NetBeans Projekt definiert

   406   \end{itemize}

   407 \item Relevante Komponenten implementieren

   408   \begin{itemize}

   409   \item jEdit Plugin f\"ur SD

   410   \item Verbindung des Plugins zu Isabelle

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

   412   \end{itemize}

   413 \end{enumerate}

   414 \end{frame}

   416 \begin{frame}\frametitle{Zusammenfassung}

   417 \pause

   418 \alert{$\mathbf{- - -}$}\\

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

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

   421 \vspace{0.3cm}

   422 \alert{$\mathbf{+ + +}$}\\

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

   424 \begin{enumerate}

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

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

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

   428 \end{enumerate}

   429 \end{frame}

   431 \begin{frame}\frametitle{}

   432 \begin{center}

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

   434 \end{center}

   435 \end{frame}

   437 \end{document}

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 20 Jun 2011 17:33:06 +0200
branch	decompose-isar
changeset 42048	6548da70f14e
parent 42046	bb864b8144a3
child 42050	2b69a774afd5
permissions	-rw-r--r--