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

 \documentclass{beamer}

 \mode<presentation>

 {

   \usetheme{Hannover}

   \setbeamercovered{transparent}

 }

 \usepackage[english]{babel}

 \usepackage[latin1]{inputenc}

 \usepackage{times}

 \usepackage{ngerman}

 \usepackage[T1]{fontenc}

 %\usepackage{graphicx}

 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

 \title[Isabelle Frontend]

 {Userinterfaces \\f\"ur Computer Theorem Prover,\\

 	Machbarkeits-Studie im \isac-Projekt

 }

 \subtitle{Bachelorarbeit Telematik}

 \author{Marco Steger}

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

   Technische Universit\"at Graz}

 \date{21.06.2011}

 %\subject{Formal specification of math assistants}

 % This is only inserted into the PDF information catalog

 % Delete this, if you do not want the table of contents to pop up at

 % the beginning of each subsection:

 \AtBeginSubsection[]

 {

   \begin{frame}<beamer>

     \frametitle{Outline}

     \tableofcontents[currentsection,currentsubsection]

   \end{frame}

 }

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

 % the following command: 

 %\beamerdefaultoverlayspecification{<+->}

 \begin{document}

 \begin{frame}

   \titlepage

 \end{frame}

 \begin{frame}

   \frametitle{Outline}

   \tableofcontents

   % You might wish to add the option [pausesections]

 \end{frame}

 \section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}

 \subsection[Isabelle]{Der Theoremprover Isabelle}

 \begin{frame}

   \frametitle{Der Theoremprover Isabelle}

 \begin{itemize}

 \item Anwendungen von Isabelle

   \begin{itemize}

   \item Mechanisieren von Mathematik Theorien

     \begin{itemize}

     \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots

     \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots          

     \item High Order Logics, Logic of Computable Functions, \dots

     \end{itemize}

 \pause

   \item Math.Grundlagen f\"ur Softwaretechnologie

     \begin{itemize}

     \item Hoare Logic, Temporal Logic of Actions, Hoare for Java

     \item Theory for Unix file-system security, for state spaces, \dots

     \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}

     \end{itemize}

   \end{itemize}

 \pause

 \item Integration von Isabelle in Entwicklungstools

   \begin{itemize}

   \item Boogie --- Verification Condition Generator

   \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs

   \item Test Case Generators (TUG) ?

   \end{itemize}

 \pause

 \item Isar, die Beweissprache von Isabelle

   \begin{itemize}

   %\item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$ 

   \item Demo 'Allgemeine Dreiecke'

 \pause

 \alert{Beweisteile asynchron interpretiert}

   \end{itemize}

 \end{itemize}

 \end{frame}

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

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

 \begin{figure}

 \begin{center}

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

 \end{center}

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

 \label{fig-reuse-ml-scala}

 \end{figure}

 \end{frame}

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

 \begin{itemize}

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

 verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert

 \pause

 \item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen)

 \pause

 \item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\

 \pause

 Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\

 \pause

 Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\

 \pause

 \alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}}

 \end{itemize}

 \end{frame}

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

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

 {\tiny

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

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

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

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

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

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

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

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

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

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

 :\\

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

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

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

 .\\

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

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

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

 .\\

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

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

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

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

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

 ./src/Pure/library.scala\\

 .\\

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

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

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

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

 .\\

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

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

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

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

 .\\

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

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

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

 .\\

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

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

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

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

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

 ./src/Pure/library.scala\\

 .\\

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

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

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

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

 .\\

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

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

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

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

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

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

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

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

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

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

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

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

 .\\

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

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

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

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

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

 }

 \end{frame}

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

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

 \begin{itemize}

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

 \pause

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

 \pause

 \item Isabelle verwendet eine Reihe davon

   \begin{itemize}

   \item der Parser ``Sidekick''

   \item Console f\"ur jEdit-Komponenten

   \item + Scala

   \item + Ml

   \item etc

   \end{itemize}

 \pause

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

 \pause

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

 \end{itemize}

 \end{frame}

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

 \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}

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

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

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

 Milestones:

 \begin{enumerate}

 \item Relevante Isabelle Komponenten identifizieren und studieren

 \item Installation der Standard-Komponenten

 \item Entwicklungsumgebung vom Isabelle-Team kopieren

 \item Relevante Komponenten implementieren

   \begin{itemize}

   \item jEdit Plugin f\"ur SD

   \item zugeh\"origen Parser

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

   \end{itemize}

 \end{enumerate}

 \end{frame}

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

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

 {\footnotesize

 \begin{tabbing}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 \>  \>$1-x$

 \end{tabbing}

 }

 \end{frame}

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

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

 Mehrere Run-Konfigurationen sind praktisch:

 \begin{itemize}

 \item Start von jEdit + Plug-ins aus NetBeans

   \begin{itemize}

   \item Exekution der fertig kompilierten jEdit.jar

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

   \end{itemize}

 \item Start von jEdit aus der Konsole

 \end{itemize}

 \vspace{0.2cm}   \pause

 Dementsprechend komplex sind die Konfigurations-Files:

 \begin{center}

 \begin{tabular}{l r l}

 build.xml          & 102 & LOCs\\

 project.xml        & 25  & LOCs\\

 project.properties & 85  & LOCs\\

 build-impl.xml     & 708 & LOCs\\

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

 \end{center}

 \end{frame}

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

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

 \begin{figure}

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

 \label{Frontend des jEdit}

 \end{figure}

 \end{frame}

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

 \begin{itemize}

 \item Aufbau: Ein Plugin besteht aus:

 \pause

 	\begin{itemize}

 	\item Source-Files: \textbf{Scala} 

 	\pause

 	\item Property file 

 	\pause

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

 	\end{itemize}

 %\pause

 %\item Bestehendes Java-Plugin in Scala transferieren

 %\pause

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

 \end{itemize}

 \end{frame}

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

 {\tiny

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

 build.xml\\

 %makedist\\

 %manifest.mf\\

 %README\_BUILD\\

 \textbf{build/*}\\

 \textbf{contrib/*}\\

 \textbf{dist/*}\\

 \textbf{plugin/}build.xml\\

 \textbf{plugin/}changes40.txt\\

 \textbf{plugin/}changes42.txt\\

 \textbf{plugin/}description.html\\

 \textbf{plugin/}IsacActions.java\\

 \textbf{plugin/}Isac.iml\\

 \textbf{plugin/}Isac.java\\

 \textbf{plugin/}IsacOptionPane.java\\

 \textbf{plugin/}IsacPlugin.java\\

 \textbf{plugin/}IsacTextArea.java\\

 \textbf{plugin/}IsacToolPanel.java\\

 \textbf{plugin/}plugin\\

 \textbf{plugin/}README.txt\\

 \textbf{nbproject/*}\\

 \textbf{src/}actions.xml\\

 \textbf{src/}changes40.txt\\

 \textbf{src/}changes42.txt\\

 \textbf{src/}description.html\\

 \textbf{src/}dockables.xml\\

 \textbf{src/}IsacActions.scala\\

 \textbf{src/}Isac.iml\\

 \textbf{src/}IsacOptionPane.scala\\

 \textbf{src/}IsacPlugin.scala\\

 \textbf{src/}Isac.props\\

 \textbf{src/}Isac.scala\\

 \textbf{src/}IsacTextArea.scala\\

 \textbf{src/}IsacToolPanel.scala\\

 \textbf{src/}manifest.mf\\

 \textbf{src/}README.txt\\

 \textbf{src/}users-guide.xml

 }

 \end{frame}

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

 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:

 \pause

 \begin{itemize}

 	\item Grunds\"atzlicher Aufbau eines GUIs

 	\pause

 	\item Kopieren von Text zwischen den einzelnen Buffers

 	\pause

 		\begin{itemize}

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

 		\end{itemize}

 	\pause

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

 	\pause

 		\begin{itemize}

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

 		\end{itemize}

 	\pause

 	\item \textit{DEMO}

 \end{itemize}

 \end{frame}

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

 \section[Summary]{Zusammenfassung}

 \begin{frame}\frametitle{Zusammenfassung}

 Folgende Milestones wurden erfolgreich abgeschlossen:

 \begin{enumerate}

 \item Relevante Isabelle Komponenten dokumentiert

 \pause

 \item Installation der Standard-Komponenten:

   \begin{itemize}

   \item Mercurial Versioncontrol

   \item NetBeans IDE

   \item Standard Isabelle Bundle

   \end{itemize}

   \pause

 \item Entwicklungsumgebung vom Isabelle-Team kopieren

   \begin{itemize}

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

   \item jEdit als NetBeans Projekt definiert

   \end{itemize}

   \pause

 \item Relevante Komponenten implementieren

   \begin{itemize}

   \item jEdit Plugin f\"ur SD

   \item Verbindung des Plugins zu Isabelle

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

   \end{itemize}

 \end{enumerate}

 \end{frame}

 \begin{frame}\frametitle{Zusammenfassung}

 \pause

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

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

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

 \vspace{0.3cm}

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

 \pause

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

 \begin{enumerate}

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

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

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

 \end{enumerate}

 \end{frame}

 \begin{frame}\frametitle{}

 \begin{center}

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

 \end{center}

 \end{frame}

 \end{document}