diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/msteger/bakk-presentation.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-isac/msteger/bakk-presentation.tex Tue Sep 17 09:50:52 2013 +0200 @@ -0,0 +1,445 @@ +% /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex + +\documentclass{beamer} +\mode +{ + \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} + \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} + +