% /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: *.jar}

%{\footnotesize

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

%{\tiny

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

%

%{\footnotesize

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

%}

%\end{frame}

%

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

%{\tiny

%./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/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}

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

{\footnotesize

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-rw-r--r-- 1 msteger root  1643 2011-03-14 17:09 swing\_thread.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'' 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{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}