1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/msteger/bakk-presentation.tex Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,445 @@
1.4 +% /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex
1.5 +
1.6 +\documentclass{beamer}
1.7 +\mode<presentation>
1.8 +{
1.9 + \usetheme{Hannover}
1.10 + \setbeamercovered{transparent}
1.11 +}
1.12 +\usepackage[english]{babel}
1.13 +\usepackage[latin1]{inputenc}
1.14 +\usepackage{times}
1.15 +\usepackage{ngerman}
1.16 +\usepackage[T1]{fontenc}
1.17 +%\usepackage{graphicx}
1.18 +
1.19 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.20 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.21 +
1.22 +\title[Isabelle Frontend]
1.23 +{Userinterfaces \\f\"ur Computer Theorem Prover,\\
1.24 + Machbarkeits-Studie im \isac-Projekt
1.25 +}
1.26 +\subtitle{Bachelorarbeit Telematik}
1.27 +
1.28 +\author{Marco Steger}
1.29 +\institute{Institut f\"ur Software Technologie\\
1.30 + Technische Universit\"at Graz}
1.31 +
1.32 +\date{21.06.2011}
1.33 +%\subject{Formal specification of math assistants}
1.34 +% This is only inserted into the PDF information catalog
1.35 +
1.36 +% Delete this, if you do not want the table of contents to pop up at
1.37 +% the beginning of each subsection:
1.38 +\AtBeginSubsection[]
1.39 +{
1.40 + \begin{frame}<beamer>
1.41 + \frametitle{Outline}
1.42 + \tableofcontents[currentsection,currentsubsection]
1.43 + \end{frame}
1.44 +}
1.45 +
1.46 +
1.47 +% If you wish to uncover everything in a step-wise fashion, uncomment
1.48 +% the following command:
1.49 +%\beamerdefaultoverlayspecification{<+->}
1.50 +
1.51 +
1.52 +\begin{document}
1.53 +\begin{frame}
1.54 + \titlepage
1.55 +\end{frame}
1.56 +
1.57 +\begin{frame}
1.58 + \frametitle{Outline}
1.59 + \tableofcontents
1.60 + % You might wish to add the option [pausesections]
1.61 +\end{frame}
1.62 +
1.63 +\section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}
1.64 +\subsection[Isabelle]{Der Theoremprover Isabelle}
1.65 +\begin{frame}
1.66 + \frametitle{Der Theoremprover Isabelle}
1.67 +\begin{itemize}
1.68 +\item Anwendungen von Isabelle
1.69 + \begin{itemize}
1.70 + \item Mechanisieren von Mathematik Theorien
1.71 + \begin{itemize}
1.72 + \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots
1.73 + \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots
1.74 + \item High Order Logics, Logic of Computable Functions, \dots
1.75 + \end{itemize}
1.76 +\pause
1.77 + \item Math.Grundlagen f\"ur Softwaretechnologie
1.78 + \begin{itemize}
1.79 + \item Hoare Logic, Temporal Logic of Actions, Hoare for Java
1.80 + \item Theory for Unix file-system security, for state spaces, \dots
1.81 + \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}
1.82 + \end{itemize}
1.83 + \end{itemize}
1.84 +\pause
1.85 +\item Integration von Isabelle in Entwicklungstools
1.86 + \begin{itemize}
1.87 + \item Boogie --- Verification Condition Generator
1.88 + \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs
1.89 + \item Test Case Generators (TUG) ?
1.90 + \end{itemize}
1.91 +\pause
1.92 +\item Isar, die Beweissprache von Isabelle
1.93 + \begin{itemize}
1.94 + %\item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$
1.95 + \item Demo 'Allgemeine Dreiecke'
1.96 +\pause
1.97 +\alert{Beweisteile asynchron interpretiert}
1.98 + \end{itemize}
1.99 +\end{itemize}
1.100 +\end{frame}
1.101 +
1.102 +\subsection[Scala-Layer]{Die Konzeption des Scala-Layers}
1.103 +\begin{frame}\frametitle{Die Konzeption des Scala-Layers}
1.104 +\begin{figure}
1.105 +\begin{center}
1.106 +\includegraphics[width=100mm]{fig-reuse-ml-scala-SD}
1.107 +\end{center}
1.108 +%\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
1.109 +\label{fig-reuse-ml-scala}
1.110 +\end{figure}
1.111 +\end{frame}
1.112 +
1.113 +\begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML}
1.114 +\begin{itemize}
1.115 +\item Das Protokoll ist \textbf{asynchron}: \\
1.116 +verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert
1.117 +\pause
1.118 +\item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen)
1.119 +\pause
1.120 +\item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\
1.121 +\pause
1.122 +Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\
1.123 +\pause
1.124 +Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\
1.125 +\pause
1.126 +\alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}}
1.127 +\end{itemize}
1.128 +\end{frame}
1.129 +
1.130 +\subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}
1.131 +
1.132 +
1.133 +\begin{frame}\frametitle{Isabelle Files: *.scala}
1.134 +{\tiny
1.135 +\textbf{\$ find -name ``*.scala''}\\
1.136 +./src/Pure/General/xml.scala\\
1.137 +./src/Pure/General/linear\_set.scala\\
1.138 +
1.139 +./src/Pure/General/symbol.scala\\
1.140 +./src/Pure/General/exn.scala\\
1.141 +./src/Pure/General/position.scala\\
1.142 +./src/Pure/General/scan.scala\\
1.143 +./src/Pure/General/xml\_data.scala\\
1.144 +./src/Pure/General/yxml.scala\\
1.145 +./src/Pure/General/markup.scala\\
1.146 +:\\
1.147 +./src/Pure/General/sha1.scala\\
1.148 +./src/Pure/General/timing.scala\\
1.149 +./src/Pure/General/pretty.scala\\
1.150 +.\\
1.151 +./src/Pure/Concurrent/volatile.scala\\
1.152 +./src/Pure/Concurrent/future.scala\\
1.153 +./src/Pure/Concurrent/simple\_thread.scala\\
1.154 +.\\
1.155 +./src/Pure/Thy/html.scala\\
1.156 +./src/Pure/Thy/completion.scala\\
1.157 +./src/Pure/Thy/thy\_header.scala\\
1.158 +./src/Pure/Thy/thy\_syntax.scala\\
1.159 +./src/Pure/Isac/isac.scala\\
1.160 +./src/Pure/library.scala\\
1.161 +.\\
1.162 +./src/Pure/Isar/keyword.scala\\
1.163 +./src/Pure/Isar/outer\_syntax.scala\\
1.164 +./src/Pure/Isar/token.scala\\
1.165 +./src/Pure/Isar/parse.scala\\
1.166 +.\\
1.167 +./src/Pure/System/gui\_setup.scala\\
1.168 +./src/Pure/System/isabelle\_system.scala\\
1.169 +./src/Pure/General/timing.scala\\
1.170 +./src/Pure/General/pretty.scala\\
1.171 +.\\
1.172 +./src/Pure/Concurrent/volatile.scala\\
1.173 +./src/Pure/Concurrent/future.scala\\
1.174 +./src/Pure/Concurrent/simple\_thread.scala\\
1.175 +.\\
1.176 +./src/Pure/Thy/html.scala\\
1.177 +./src/Pure/Thy/completion.scala\\
1.178 +./src/Pure/Thy/thy\_header.scala\\
1.179 +./src/Pure/Thy/thy\_syntax.scala\\
1.180 +./src/Pure/Isac/isac.scala\\
1.181 +./src/Pure/library.scala\\
1.182 +.\\
1.183 +./src/Pure/Isar/keyword.scala\\
1.184 +./src/Pure/Isar/outer\_syntax.scala\\
1.185 +./src/Pure/Isar/token.scala\\
1.186 +./src/Pure/Isar/parse.scala\\
1.187 +.\\
1.188 +./src/Pure/System/gui\_setup.scala\\
1.189 +./src/Pure/System/isabelle\_system.scala\\
1.190 +./src/Pure/System/swing\_thread.scala\\
1.191 +./src/Pure/System/download.scala\\
1.192 +./src/Pure/System/session\_manager.scala\\
1.193 +./src/Pure/System/standard\_system.scala\\
1.194 +./src/Pure/System/isabelle\_syntax.scala\\
1.195 +./src/Pure/System/session.scala\\
1.196 +./src/Pure/System/platform.scala\\
1.197 +./src/Pure/System/cygwin.scala\\
1.198 +./src/Pure/System/event\_bus.scala\\
1.199 +./src/Pure/System/isabelle\_process.scala\\
1.200 +.\\
1.201 +./src/Pure/PIDE/document.scala\\
1.202 +./src/Pure/PIDE/markup\_tree.scala\\
1.203 +./src/Pure/PIDE/text.scala\\
1.204 +./src/Pure/PIDE/command.scala\\
1.205 +./src/Pure/PIDE/isar\_document.scala
1.206 +}
1.207 +\end{frame}
1.208 +
1.209 +
1.210 +
1.211 +\subsection[jEdit]{Das Frontend: jEdit und ``plugins''}
1.212 +\begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''}
1.213 +\begin{itemize}
1.214 +\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.''}
1.215 +\pause
1.216 +\item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt
1.217 +\pause
1.218 +\item Isabelle verwendet eine Reihe davon
1.219 + \begin{itemize}
1.220 + \item der Parser ``Sidekick''
1.221 + \item Console f\"ur jEdit-Komponenten
1.222 + \item + Scala
1.223 + \item + Ml
1.224 + \item etc
1.225 + \end{itemize}
1.226 +\pause
1.227 +\item jEdit ist ``open source'' mit gro\3er Community
1.228 +\pause
1.229 +\item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle
1.230 +\end{itemize}
1.231 +\end{frame}
1.232 +
1.233 +\section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)}
1.234 +\subsection[Aufgabenstellung]{Definition der Aufgabenstellung}
1.235 +\begin{frame}\frametitle{Definition der Aufgabenstellung}
1.236 +Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured~derivations'' (SD) in Isabelle.\\
1.237 +
1.238 +\textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\
1.239 +
1.240 +Milestones:
1.241 +\begin{enumerate}
1.242 +\item Relevante Isabelle Komponenten identifizieren und studieren
1.243 +\item Installation der Standard-Komponenten
1.244 +\item Entwicklungsumgebung vom Isabelle-Team kopieren
1.245 +\item Relevante Komponenten implementieren
1.246 + \begin{itemize}
1.247 + \item jEdit Plugin f\"ur SD
1.248 + \item zugeh\"origen Parser
1.249 + \item nicht vorgesehen: SD-Interpreter in Isar (SML)
1.250 + \end{itemize}
1.251 +\end{enumerate}
1.252 +\end{frame}
1.253 +
1.254 +%\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
1.255 +\begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}
1.256 +{\footnotesize
1.257 +\begin{tabbing}
1.258 +123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
1.259 +\>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
1.260 +\> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
1.261 +\>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
1.262 +\> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
1.263 +\>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
1.264 +\> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
1.265 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
1.266 +\> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
1.267 +\> \>$\equiv$\>\vdots\\
1.268 +\> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
1.269 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
1.270 +\> \> \>$1 + -1 * x$\\
1.271 +\>\dots\>$1 + -1 * x$\\
1.272 +\>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
1.273 +\> \>$1-x$
1.274 +\end{tabbing}
1.275 +}
1.276 +\end{frame}
1.277 +
1.278 +\subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE}
1.279 +\begin{frame}\frametitle{Konfiguration in NetBeans}
1.280 +Mehrere Run-Konfigurationen sind praktisch:
1.281 +\begin{itemize}
1.282 +\item Start von jEdit + Plug-ins aus NetBeans
1.283 + \begin{itemize}
1.284 + \item Exekution der fertig kompilierten jEdit.jar
1.285 + \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen !
1.286 + \end{itemize}
1.287 +\item Start von jEdit aus der Konsole
1.288 +\end{itemize}
1.289 +\vspace{0.2cm} \pause
1.290 +Dementsprechend komplex sind die Konfigurations-Files:
1.291 +\begin{center}
1.292 +\begin{tabular}{l r l}
1.293 +build.xml & 102 & LOCs\\
1.294 +project.xml & 25 & LOCs\\
1.295 +project.properties & 85 & LOCs\\
1.296 +build-impl.xml & 708 & LOCs\\
1.297 + & & (teilw. automatisch generiert)\end{tabular}
1.298 +\end{center}
1.299 +\end{frame}
1.300 +
1.301 +\subsection[Implementation]{Komponenten zur Implementation von SD}
1.302 +
1.303 +\begin{frame}\frametitle{Die Konzeption des Scala-Layers}
1.304 +\begin{figure}
1.305 +\includegraphics[width=100mm]{fig-jedit-plugins-SD}
1.306 +\label{Frontend des jEdit}
1.307 +\end{figure}
1.308 +\end{frame}
1.309 +
1.310 +\begin{frame}\frametitle{jEdit-Plugin}
1.311 +\begin{itemize}
1.312 +\item Aufbau: Ein Plugin besteht aus:
1.313 +\pause
1.314 + \begin{itemize}
1.315 + \item Source-Files: \textbf{Scala}
1.316 + \pause
1.317 + \item Property file
1.318 + \pause
1.319 + \item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)
1.320 + \end{itemize}
1.321 +%\pause
1.322 +%\item Bestehendes Java-Plugin in Scala transferieren
1.323 +%\pause
1.324 +%\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren
1.325 +\end{itemize}
1.326 +\end{frame}
1.327 +
1.328 +\begin{frame}\frametitle{Sources des jEdit Plugins}
1.329 +{\tiny
1.330 +src/Tools/jEditC\textbf{\$ ls -l *}\\
1.331 +build.xml\\
1.332 +%makedist\\
1.333 +%manifest.mf\\
1.334 +%README\_BUILD\\
1.335 +\textbf{build/*}\\
1.336 +\textbf{contrib/*}\\
1.337 +\textbf{dist/*}\\
1.338 +\textbf{plugin/}build.xml\\
1.339 +\textbf{plugin/}changes40.txt\\
1.340 +\textbf{plugin/}changes42.txt\\
1.341 +\textbf{plugin/}description.html\\
1.342 +\textbf{plugin/}IsacActions.java\\
1.343 +\textbf{plugin/}Isac.iml\\
1.344 +\textbf{plugin/}Isac.java\\
1.345 +\textbf{plugin/}IsacOptionPane.java\\
1.346 +\textbf{plugin/}IsacPlugin.java\\
1.347 +\textbf{plugin/}IsacTextArea.java\\
1.348 +\textbf{plugin/}IsacToolPanel.java\\
1.349 +\textbf{plugin/}plugin\\
1.350 +\textbf{plugin/}README.txt\\
1.351 +\textbf{nbproject/*}\\
1.352 +\textbf{src/}actions.xml\\
1.353 +\textbf{src/}changes40.txt\\
1.354 +\textbf{src/}changes42.txt\\
1.355 +\textbf{src/}description.html\\
1.356 +\textbf{src/}dockables.xml\\
1.357 +\textbf{src/}IsacActions.scala\\
1.358 +\textbf{src/}Isac.iml\\
1.359 +\textbf{src/}IsacOptionPane.scala\\
1.360 +\textbf{src/}IsacPlugin.scala\\
1.361 +\textbf{src/}Isac.props\\
1.362 +\textbf{src/}Isac.scala\\
1.363 +\textbf{src/}IsacTextArea.scala\\
1.364 +\textbf{src/}IsacToolPanel.scala\\
1.365 +\textbf{src/}manifest.mf\\
1.366 +\textbf{src/}README.txt\\
1.367 +\textbf{src/}users-guide.xml
1.368 +}
1.369 +\end{frame}
1.370 +
1.371 +\begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}
1.372 +Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:
1.373 +\pause
1.374 +\begin{itemize}
1.375 + \item Grunds\"atzlicher Aufbau eines GUIs
1.376 + \pause
1.377 + \item Kopieren von Text zwischen den einzelnen Buffers
1.378 + \pause
1.379 + \begin{itemize}
1.380 + \item \alert{Somit auch Zugriff auf andere Plugins!}
1.381 + \end{itemize}
1.382 + \pause
1.383 + \item Ansatz f\"ur die Einbindung des SD-Parsers
1.384 + \pause
1.385 + \begin{itemize}
1.386 + \item Zugriff auf Isabelle-Pure: \alert{parsen von SD parallel zu Isabelle/Isar}
1.387 + \end{itemize}
1.388 + \pause
1.389 + \item \textit{DEMO}
1.390 +\end{itemize}
1.391 +\end{frame}
1.392 +
1.393 +
1.394 +%\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
1.395 +
1.396 +\section[Summary]{Zusammenfassung}
1.397 +\begin{frame}\frametitle{Zusammenfassung}
1.398 +Folgende Milestones wurden erfolgreich abgeschlossen:
1.399 +\begin{enumerate}
1.400 +\item Relevante Isabelle Komponenten dokumentiert
1.401 +\pause
1.402 +\item Installation der Standard-Komponenten:
1.403 + \begin{itemize}
1.404 + \item Mercurial Versioncontrol
1.405 + \item NetBeans IDE
1.406 + \item Standard Isabelle Bundle
1.407 + \end{itemize}
1.408 + \pause
1.409 +\item Entwicklungsumgebung vom Isabelle-Team kopieren
1.410 + \begin{itemize}
1.411 + \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
1.412 + \item jEdit als NetBeans Projekt definiert
1.413 + \end{itemize}
1.414 + \pause
1.415 +\item Relevante Komponenten implementieren
1.416 + \begin{itemize}
1.417 + \item jEdit Plugin f\"ur SD
1.418 + \item Verbindung des Plugins zu Isabelle
1.419 + \item zugeh\"origen Parser: nur ein Test in SML
1.420 + \end{itemize}
1.421 +\end{enumerate}
1.422 +\end{frame}
1.423 +
1.424 +\begin{frame}\frametitle{Zusammenfassung}
1.425 +\pause
1.426 +\alert{$\mathbf{- - -}$}\\
1.427 +Aus Zeitgr\"unden nicht m\"oglich: ein komplettes SD-Plugin;\\
1.428 +dazu w\"are auch ein Interpreter auf der ML-Seite n\"otig.\\
1.429 +\vspace{0.3cm}
1.430 +\alert{$\mathbf{+ + +}$}\\
1.431 +\pause
1.432 +Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen:
1.433 +\begin{enumerate}
1.434 +\item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
1.435 +\item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend
1.436 +\item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).
1.437 +\end{enumerate}
1.438 +\end{frame}
1.439 +
1.440 +\begin{frame}\frametitle{}
1.441 +\begin{center}
1.442 +\LARGE{Danke f\"ur die Aufmerksamkeit !}
1.443 +\end{center}
1.444 +\end{frame}
1.445 +
1.446 +\end{document}
1.447 +
1.448 +