1.1 --- a/doc-src/isac/msteger/bakk-presentation.tex Tue May 31 10:39:02 2011 +0200
1.2 +++ b/doc-src/isac/msteger/bakk-presentation.tex Tue Jun 14 18:03:14 2011 +0200
1.3 @@ -9,6 +9,7 @@
1.4 \usepackage[english]{babel}
1.5 \usepackage[latin1]{inputenc}
1.6 \usepackage{times}
1.7 +\usepackage{ngerman}
1.8 \usepackage[T1]{fontenc}
1.9 %\usepackage{graphicx}
1.10
1.11 @@ -17,7 +18,7 @@
1.12
1.13 \title[Isabelle Frontend]
1.14 {Userinterfaces \\f\"ur Computer Theorem Prover,\\
1.15 - Machbarkeits-Studie im Isac-Projekt
1.16 + Machbarkeits-Studie im \isac-Projekt
1.17 }
1.18 \subtitle{Bachelorarbeit Telematik}
1.19
1.20 @@ -56,31 +57,7 @@
1.21 % You might wish to add the option [pausesections]
1.22 \end{frame}
1.23
1.24 -\section[Isabelle]{Der Theoremprover Isabelle}
1.25 -%\begin{frame}
1.26 -% \frametitle{The ideal math assistant \dots}
1.27 -%\begin{enumerate}
1.28 -%\item \alert{guides the user} step by step towards a solution\\
1.29 -%\uncover<2->{\textit{
1.30 -%Watching teachers calculate step by step is boring.\\
1.31 -%Operating on formulas by hand is hard, too.\\
1.32 -%Software can support {\bf independent learning}.
1.33 -%}}
1.34 -%\item \alert{checks user input} as generous and liberal as possible\\
1.35 -%\uncover<3->{\textit{
1.36 -%Active learning by {\bf trial and error} ist most effective.\\
1.37 -%Programmers cannot foresee learners' input.\\
1.38 -%Theorem provers provide most general checking.
1.39 -%}}
1.40 -%\item \alert{explains steps} on request by the user\\
1.41 -%\uncover<4->{\textit{
1.42 -%Programmers also cannot foresee learners' questions.\\
1.43 -%A system must be {\bf transparent} for casual questions.\\
1.44 -%LCF-style provers have knowledge human readable.
1.45 -%}}
1.46 -%\end{enumerate}
1.47 -%\end{frame}
1.48 -
1.49 +\section[Isabelle]{Einleitung: Der Theoremprover Isabelle}
1.50 \begin{frame}
1.51 \frametitle{Der Theoremprover Isabelle}
1.52 \begin{itemize}
1.53 @@ -92,6 +69,7 @@
1.54 \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots
1.55 \item High Order Logics, Logic of Computable Functions, \dots
1.56 \end{itemize}
1.57 +\pause
1.58 \item Math.Grundlagen f\"ur Softwaretechnologie
1.59 \begin{itemize}
1.60 \item Hoare Logic, Temporal Logic of Actions, Hoare for Java
1.61 @@ -99,36 +77,224 @@
1.62 \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}
1.63 \end{itemize}
1.64 \end{itemize}
1.65 +\pause
1.66 \item Integration von Isabelle in Entwicklungstools
1.67 \begin{itemize}
1.68 \item Boogie --- Verification Condition Generator
1.69 - \item ? Test Case Generators (TUG) ?
1.70 - \item \dots ???
1.71 + \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs
1.72 + \item Test Case Generators (TUG) ?
1.73 \end{itemize}
1.74 +\pause
1.75 \item Isar, die Beweissprache von Isabelle
1.76 + \begin{itemize}
1.77 + \item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$
1.78 \pause
1.79 - \begin{itemize}
1.80 - \item Demo
1.81 +\alert{Beweisteile asynchron interpretiert}
1.82 \end{itemize}
1.83 \end{itemize}
1.84 \end{frame}
1.85
1.86 -\section[Komponenten]{Komponenten des kommenden Isabelle Frontends}
1.87 -\subsection[Scala]{Scala und ``Actors''}
1.88 -\subsection[jEdit]{jEdit und ``Plugins''}
1.89 -\subsection[Integration]{Integration von Scala und ML}
1.90 +\section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}
1.91 +\subsection[Scala-Layer]{Die Konzeption des Scala-Layers}
1.92 +\begin{frame}\frametitle{Die Konzeption des Scala-Layers}
1.93 +\begin{figure}
1.94 +\begin{center}
1.95 +\includegraphics[width=75mm]{fig/archi/fig-reuse-ml-scala-SD}
1.96 +\end{center}
1.97 +%\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
1.98 +\label{fig-reuse-ml-scala}
1.99 +\end{figure}
1.100 +\end{frame}
1.101
1.102 -\section[NetBeans]{Installation der Komponenten in NetBeans}
1.103 -\subsection[TODO]{TODO}
1.104 +\begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML}
1.105 +\begin{itemize}
1.106 +\item Das Protokoll ist \textbf{asynchron}: \\
1.107 +verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert
1.108 +\pause
1.109 +\item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen)
1.110 +\pause
1.111 +\item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\
1.112 +\pause
1.113 +Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\
1.114 +\pause
1.115 +Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\
1.116 +\pause
1.117 +\alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}}
1.118 +\end{itemize}
1.119 +\end{frame}
1.120
1.121 -\section[NetBeans]{Vorbereitung f\"ur ``structured derivations''}
1.122 -\subsection[Parsen]{Parsen von Isar-Texten}
1.123 +\subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}
1.124 +\begin{frame}\frametitle{Isabelle Files: *.jar}
1.125 +{\footnotesize
1.126 +----- for ``isabelle jedit \&''; contained in Isabelle\_bundle}\\
1.127 +{\tiny
1.128 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar\\
1.129 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar\\
1.130 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar\\
1.131 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar\\
1.132 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \alert{$\;\;\;\;\;\;\;\;\;\;\;\Longleftarrow$ entry to SML}\\
1.133 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar\\
1.134 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar\\
1.135 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar\\
1.136 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar\\
1.137 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar\\
1.138 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar\\
1.139 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar\\
1.140 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar\\
1.141 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar\\
1.142 +./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar\\
1.143
1.144 -\section*{Summary}
1.145 -\begin{frame}
1.146 - \frametitle<presentation>{Summary}
1.147 +{\footnotesize
1.148 +----- scala system; contained in Isabelle\_bundle}\\
1.149 +./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar\\
1.150 +./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar\\
1.151 +./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar\\
1.152 +./contrib/scala-2.8.1.final/lib/scala-compiler.jar\\
1.153 +./contrib/scala-2.8.1.final/lib/scalap.jar\\
1.154 +./contrib/scala-2.8.1.final/lib/scala-swing.jar\\
1.155 +./contrib/scala-2.8.1.final/lib/scala-library.jar\\
1.156 +./contrib/scala-2.8.1.final/lib/jline.jar\\
1.157 +./contrib/scala-2.8.1.final/lib/scala-dbc.jar\\
1.158 +./contrib/scala-2.8.1.final/src/scala-library-src.jar\\
1.159 +./contrib/scala-2.8.1.final/src/scala-swing-src.jar\\
1.160 +./contrib/scala-2.8.1.final/src/scala-compiler-src.jar\\
1.161 +./contrib/scala-2.8.1.final/src/scala-dbc-src.jar\\
1.162 +./contrib/scala-2.8.1.final/src/sbaz-src.jar\\
1.163 +}
1.164 +\end{frame}
1.165
1.166 - Summary TODO
1.167 +\begin{frame}\frametitle{Isabelle Files: *.scala}
1.168 +{\tiny
1.169 +./src/Pure/General/xml.scala\\
1.170 +./src/Pure/General/linear\_set.scala\\
1.171 +./src/Pure/General/symbol.scala\\
1.172 +./src/Pure/General/exn.scala\\
1.173 +./src/Pure/General/position.scala\\
1.174 +./src/Pure/General/scan.scala\\
1.175 +./src/Pure/General/xml\_data.scala\\
1.176 +./src/Pure/General/yxml.scala\\
1.177 +./src/Pure/General/markup.scala\\
1.178 +./src/Pure/General/sha1.scala\\
1.179 +./src/Pure/General/timing.scala\\
1.180 +./src/Pure/General/pretty.scala\\
1.181 +.\\
1.182 +./src/Pure/Concurrent/volatile.scala\\
1.183 +./src/Pure/Concurrent/future.scala\\
1.184 +./src/Pure/Concurrent/simple\_thread.scala\\
1.185 +.\\
1.186 +./src/Pure/Thy/html.scala\\
1.187 +./src/Pure/Thy/completion.scala\\
1.188 +./src/Pure/Thy/thy\_header.scala\\
1.189 +./src/Pure/Thy/thy\_syntax.scala\\
1.190 +./src/Pure/Isac/isac.scala\\
1.191 +./src/Pure/library.scala\\
1.192 +.\\
1.193 +./src/Pure/Isar/keyword.scala\\
1.194 +./src/Pure/Isar/outer\_syntax.scala\\
1.195 +./src/Pure/Isar/token.scala\\
1.196 +./src/Pure/Isar/parse.scala\\
1.197 +.\\
1.198 +./src/Pure/System/gui\_setup.scala\\
1.199 +./src/Pure/System/isabelle\_system.scala\\
1.200 +./src/Pure/System/swing\_thread.scala\\
1.201 +./src/Pure/System/download.scala\\
1.202 +./src/Pure/System/session\_manager.scala\\
1.203 +./src/Pure/System/standard\_system.scala\\
1.204 +./src/Pure/System/isabelle\_syntax.scala\\
1.205 +./src/Pure/System/session.scala\\
1.206 +./src/Pure/System/platform.scala\\
1.207 +./src/Pure/System/cygwin.scala\\
1.208 +./src/Pure/System/event\_bus.scala\\
1.209 +./src/Pure/System/isabelle\_process.scala\\
1.210 +.\\
1.211 +./src/Pure/PIDE/document.scala\\
1.212 +./src/Pure/PIDE/markup\_tree.scala\\
1.213 +./src/Pure/PIDE/text.scala\\
1.214 +./src/Pure/PIDE/command.scala\\
1.215 +./src/Pure/PIDE/isar\_document.scala
1.216 +}
1.217 +\end{frame}
1.218 +
1.219 +\begin{frame}\frametitle{*.scala --- *.ML}
1.220 +{\footnotesize
1.221 +isabisac\$ ls -l src/Pure/System/\\
1.222 +-rw-r--r-- 1 msteger root 3987 2011-03-14 17:09 cygwin.scala\\
1.223 +-rw-r--r-- 1 msteger root 1486 2011-03-14 17:09 download.scala\\
1.224 +-rw-r--r-- 1 msteger root 1296 2011-03-14 17:09 event\_bus.scala\\
1.225 +-rw-r--r-- 1 msteger root 1830 2011-03-14 17:09 gui\_setup.scala\\
1.226 +-rw-r--r-- 1 msteger root 5722 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{ML}\\
1.227 +-rw-r--r-- 1 msteger root 1059 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{scala}\\
1.228 +-rw-r--r-- 1 msteger root 1659 2011-03-14 17:09 isabelle\_syntax.scala\\
1.229 +-rw-r--r-- 1 msteger root 2087 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{ML}\\
1.230 +-rw-r--r-- 1 msteger root 1168 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{scala}\\
1.231 +-rw-r--r-- 1 msteger root 5935 2011-03-14 17:09 isar.ML\\
1.232 +-rw-r--r-- 1 msteger root 1989 2011-03-14 17:09 platform.scala\\
1.233 +-rw-r--r-- 1 msteger root 1427 2011-03-14 17:09 session\_manager.scala\\
1.234 +-rw-r--r-- 1 msteger root 3833 2011-03-14 17:09 \alert{session}.\textbf{ML}\\
1.235 +-rw-r--r-- 1 msteger root 9172 2011-03-14 17:09 \alert{session}.\textbf{scala}\\
1.236 +-rw-r--r-- 1 msteger root 9086 2011-03-14 17:09 standard\_system.scala\\
1.237 +-rw-r--r-- 1 msteger root 1643 2011-03-14 17:09 swing\_thread.scala\\
1.238 +
1.239 +}
1.240 +\end{frame}
1.241 +
1.242 +\subsection[jEdit]{Das Frontend: jEdit und ``plugins''}
1.243 +\begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''}
1.244 +\begin{itemize}
1.245 +\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.246 +\pause
1.247 +\item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt
1.248 +\pause
1.249 +\item Isabelle verwendet eine Reihe davon
1.250 + \begin{itemize}
1.251 + \item der Parser ``Sidekick''
1.252 + \item Console f\"ur jEdit-Komponenten
1.253 + \item + Scala
1.254 + \item + Ml
1.255 + \item etc
1.256 + \end{itemize}
1.257 +\pause
1.258 +\item jEdit ist ``open source'' mit gro\3er Community
1.259 +\pause
1.260 +\item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle
1.261 +\end{itemize}
1.262 +\end{frame}
1.263 +
1.264 +\section[Projektarbeit]{Projektarbeit: Vorbereitungen f\"ur ``structured derivations''}
1.265 +\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
1.266 +\begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}
1.267 +{\footnotesize
1.268 +\begin{tabbing}
1.269 +123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
1.270 +\>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
1.271 +\> \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
1.272 +\>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
1.273 +\> \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
1.274 +\>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
1.275 +\> \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
1.276 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
1.277 +\> \> \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
1.278 +\> \>$\equiv$\>\vdots\\
1.279 +\> \> \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
1.280 +\> \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$ \\
1.281 +\> \> \>$1 + -1 * x$\\
1.282 +\>\dots\>$1 + -1 * x$\\
1.283 +\>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
1.284 +\> \>$1-x$
1.285 +\end{tabbing}
1.286 +}
1.287 +\end{frame}
1.288 +
1.289 +\subsection[NetBeans]{Aufsetzen des Projektes in der NetBeans IDE}
1.290 +\subsection[Implementation]{Komponenten zur von SD}
1.291 +\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
1.292 +
1.293 +\section[Summary]{Zusammenfassung}
1.294 +\begin{frame}\frametitle{Zusammenfassung}
1.295 + Zusammenfassung TODO
1.296 +\end{frame}
1.297 +
1.298 +\begin{frame}\frametitle{}
1.299 \end{frame}
1.300
1.301 \end{document}