1 \documentclass[a4paper,12pt]{article}
3 \usepackage[ngerman]{babel}
4 \usepackage[utf8]{inputenc}
7 \bibliographystyle{alpha}
9 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
10 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
14 \title{\Large {\bf Verbindung von 'Computation' und 'Deduction' im \isac{}-System}\\~\\
15 Projektpraktikum am Institut für Computersprachen, TU Wien}
16 \author{Mathias Lehnfeld\\
17 {\tt mathias.lehnfeld@gmx.at}}
24 \section{Zur Aufgabenstellung}
25 Das \sisac{}-Projekt entwickelt einen {\it math assistant} aufbauend auf den
26 {\it theorem prover} Isabelle. Der Kern des \sisac{}-Systems ist ein
27 {\it Lucas-Interpreter}, der automatisch Benutzerführung für schrittweises
28 Problemlösen erzeugt: Der nächste Schritt wird von einem Programm
29 berechnet ({\it computation}); {\it deduction} wird gefordert, wenn der Benutzer
30 eine Formel eingibt (die Ableitbarkeit der Formel aus dem {\it context} ist
33 Die Aufgabenstellung im Rahmen des Projektpraktikums besteht darin, das
34 in Isabelle verfügbare Konzept {\it context} in den Lucas-Interpreter
35 einzubauen. Dies schließt grundlegende Design-Überlegungen ein, verlangt
36 tiefes Eindringen in den umfangreichen Code von zwei Softwareprodukten,
37 {\it Isabelle} und \sisac{} und bedeutet daher Zusammenarbeit mit den jeweiligen
40 Ein erfolgreicher Einbau der Isabelle-{\it context}s in den
41 Lucas-Interpreter wird \sisac{}s Fähigkeit, Benutzereingaben zu
42 interpretieren, wesentlich erweitern: {\it context}s stellen Isabelles
43 automatischen Beweisern die notwendigen Daten bereit.
47 \section{Planung des Projektes}
48 \subsection{Ist-Zustand vor dem Projekt}
49 Das Isabelle Konzept der {\it context}s findet derzeit in \sisac{} noch keine Verwendung. Dadurch entstehen gewisse Einschränkungen bezüglich der Interpretation durch den Lucas-Interpreter, weil Rechenschritte nicht unter Berücksichtigung aller Faktoren ihres Kontexts betrachtet werden können. Derzeit werden Zusicherungen und Umgebungsdaten in einer \sisac{}-spezifischen Datenstruktur verwaltet, die Zugriffe auf Isabelles Prover nicht direkt unterstützen.
51 \subsection{Geplanter Soll-Zustand nach dem Projekt}
52 \sisac{}s Lucas-Interpreter ist nun schlanker und nimmt Isabelles {\it context}s bei der Interpretation von Benutzereingaben in Anspruch. Spezifikationen werden mit Isabelles eigenen Datenstrukturen verwaltet. Zusicherungen und Typen von Variablen werden im Lucas-Interpreter in {\it context}s behandelt.
54 \subsection{Zeitplanung f\"ur das Projekt}
55 Die Planung f\"ur das Projekt sah folgende Meilensteine vor:
57 \item \textbf{Voraussetzungen zum Arbeitsbeginn schaffen} (10.Feb. -- 28.Feb)\\
59 \item \textbf{\isac{} auf die letzte Isabelle-Release updaten} (TODO)\\
66 \section{Konzepte und L\"osungen}
67 \subsection{Architektur von \isac}
68 Die Grafik auf Seite p.\pageref{architektur} gibt einen \"Uberblick \"uber die Architektur von \sisac:
72 \includegraphics[width=120mm]{overview.pdf}
74 \caption{Lucas-interpreter und Isabelle}
77 Die Mathematik-Engine von \sisac{} ist nach dem Konzept eines ``Lucas-Interpreters'' (LI) gebaut. Ein LI interpretiert drei Arten von Daten:
79 \item\label{spec}\textbf{Spezifikationen}: diese beschreiben ein Problem der angewandten Mathematik durch die Ein-Ausgabe-Daten, die ``Precondition'' (Pr\"adikate auf den Eingabe-Daten) und eine eine ``Postcondition'' (eine Relation zwischen Ein- und Ausgabe-Daten). Spezifikationen stellen den \textit{applikations-orientierten} Aspekt der Mathematik dar.
80 \item \textbf{Programme}: beschreiben den Algorithmus zur L\"osung des spezifizierten Problems. \sisac's programmsprache ist funktional und hat keine Ein-Ausgabe-Statements \cite{plmms10}. Sie kann aber auf Funktionalit\"aten des Computer Theorem Provers (CTP) Isabelle \cite{Nipkow-Paulson-Wenzel:2002} zugreifen. Programme stellen den \textit{algorithmischen} Aspekt der Mathematik dar.
81 \item \textbf{Theorien}: beinhalten die Definitionen, Axiome und Theoreme, die einer bestimmten Rechnung der angewandten Mathematik zugrundeliegen. \sisac{} verwendet die ``theories'' von Isabelle in vollem Umfangt. Theorien stellen den \textit{deduktiven} Aspekt der Mathematik dar.
84 Die Funktionalit\"at eines LI kann in kurzer Form so beschrieben werden \footnote{Siehe http://www.ist.tugraz.at/isac/index.php/Description}:
91 \subsection{Isabelles Konzept von ``contexts''}
92 Die Beschreibung dieses bew\"ahrten Konzeptes findet sich in einem internen Papier zur Implementation von Isabelles Beweissprache Isar \cite{isar-impl}. Isabelle stellt einen sehr generellen Funktor zur Verf\"ugung:
97 structure ContextData = {Proof\_Data}\\
98 \>~({type T} = term list\\
99 \>\>{fun init \_} = []);\\
101 fun insert\_assumptions asms = \\
102 \>\>\>ContextData{.map} (fn xs => distinct (data@xs));\\
104 fun get\_assumptions ctxt = ContextData{.get} ctxt;\\
107 val declare\_constraints : \\
108 \>\>\>term -> Proof.context -> Proof.context
111 Das Einzige, was die Definition eines''contexts'' braucht, sind eine Spezifikation eines Typs \textit{type T} und einer Funktion \textit{fun init \_} f\"ur den Funktor \textit{Proof\_Data}. Dieser stellt dann die Zugriffsfunktionen \textit{ContextData.map} und \textit{ContextData.get} zur Verf\"ugung.
113 Die Funktion \textit{declare\_constraints} liefert eine wichtige Funktionalit\"at: Ein \textit{term} angewandt auf einen \textit{Proof.context} ergibt einen neuen \textit{Proof.context}, der f\"ur das Parsen von Strings verwendet werden kann:
116 xx\=xx\=xx\=xx\=xx\=\kill
117 fun parseNEW ctxt str = \\
118 \>\>\>SOME ({Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
119 \>\>\>handle \_ => NONE;
122 \textit{Syntax.read\_term ctxt} entnimmt den ``context'' die Typinformation, die vorher durch \textit{declare\_constraints} zugef\"uhrt wurde. Da die \textit{fun parse} vor Beginn dieses Projektes keine ``contexts'' zur Verf\"ugung hatte, setzte sie mittels \textit{typ\_a2real} alle unbestimmten Typen einfach auf \textit{real}:
125 xx\=xx\=xx\=xx\=xx\=\kill
126 fun parse thy str =\\
127 \>(let val t = ({typ\_a2real} o numbers\_to\_string)\\
128 \>\>\>\>({Syntax.read\_term\_global thy} str)\\
129 \>\>in SOME (cterm\_of thy t) end)\\
130 \>\>\>handle \_ => NONE;\\
134 \subsection{Die Initialisierung von ``contexts''}\label{init-ctxt}
135 ``Contexts'' werden anzwei Stellen von Lucas-Interpretation initialisiert: am Beginn der Spezifikations-Phase und zu Beginn der L\"ose-Phase.
138 \item\label{init-ctxt-spec}{Die Spezifikations-Phase} dient der Erstellung einer formalen Spezifikation (siehe \ref{spec})\footnote{Da bekannterma\3en formales Spezifizieren schwierig ist, kann es durch entsprechende Dialog-Einstellung dem LI \"uberlassen werden.}. Der ``context'' wird initialisiert mit den Typdeklarationen aller vorkommenden Variablen mittels \textit{declare\_constraints}.
140 Im Falle eines Rootproblems kommen die Variablen von einer ``formalization'', einer Kurzbeschreibung der Eingabe-Daten durch einen Autor. Im Falle eines Subproblems kommen die Variablen von den ``actual arguments'' des Subprogrammes.
142 \item\label{init-ctxt-solve}{Die L\"ose-Phase} erzeugt die Rechenschritte aus dem spezifizierten Programm. Zu Beginn der Interpretation des Programmes wird der ``context'' initialisiert mit
144 \item den Typdeklarationen aller in der Spezifikation vorkommenden Variablen mittels \textit{declare\_constraints}
145 \item den ``preconditions'' des (interaktiv oder automatisch) spezifizierten Programmes, genauer: mit den ``preconditions'' des zugeh\"origen Guards, der meist gleich der Spezifikation ist
150 \subsection{Aufbau von ``contexts'' in der Interpretation}\label{partiality}
151 W\"ahrend der Interpretation eines Programmes baut der Lucas-Interpreter einen ``context'' auf, indem er alle relevanten ``preconditions'', andere Pr\"adikate -- insbesonders ``partiality conditions'' einsammelt. Eine ``partiality condition'' ist zum Beispiel $x\not=0$, die Division durch $0$ verhindert.
153 Am Ende eines Programmes soll der ``context'' hinreichend logische Information enthalten, sodass Isabelles automatische Beweise die ``postcondition'' automatisch beweisen k\"onnen (das ist eine k\"unftige Entwicklungsaufgabe~!).
155 \subsection{Transfer von ``contexts'' aus Subprogrammen}\label{transfer}
156 ``contexts'' folgen den \"ublichen Scope-Regeln von Programmsprachen mit Blockstruktur, wie schon die Initialisierung von ``contexts'' gezeigt hat. Die Behandlung von ``contexts'' bei der R\"uckkehr aus Subprogrammen erfolgt durch folgende Funktionen:
159 xx\=xx\=xx\=xx\=xx\=\kill
160 fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\
162 \>\> val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\
163 \>\> fun transfer [] to\_ctxt = to\_ctxt\\
164 \>\>\> | transfer (from\_asm::fas) to\_ctxt =\\
165 \>\>\>\>\> if inter op = (vars from\_asm) to\_vars = []\\
166 \>\>\>\>\> then transfer fas to\_ctxt\\
167 \>\>\>\>\> else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\
168 \> in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\
171 Folgende Daten werden aus dem Sub-``context'' in den ``context'' des aufrufenden Programmes zur\"uckgegeben:
173 \item die R\"uckgabewerte des Subprogrammes, soferne sie vom Typ \textit{bool} sind
174 \item alle \textit{assumptions}, die eine Variable enthalten, die auch ein R\"uckgabewerte enth\"alt
175 \item alle \textit{assumptions}, die eine Variable enthalten, die in einem Term des aufrufenden Programmes enthalten sind\footnote{In diesem Punkt sind die Scope-Regeln schw\"acher als sonst bei Subprogrammen; \begin{tabbing}
177 \`$\mathit{(some)}\;\mathit{assumptions}$\\
178 $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
179 % \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
180 %\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
181 %\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
182 \>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\
183 \`$x\not=3\land x\not=0$\\
184 \>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
185 \>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
186 %\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
187 %\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
188 \>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
189 \>\>$-6 * x + 5 * x ^ 2 = 0$ \\
190 \>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
191 \>\>$[x = 0, x = \frac{6}{5}]$ \\
192 \`$x = 0\land x = \frac{6}{5}$\\
193 \>$[{x = 0}, x = \frac{6}{5}]$ \\
194 \`{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
195 \>$[x = \frac{6}{5}]$ \\
198 der Unterschied begr\"undet sich darin, dass Rechnungen vorzugsweise mit Variablennamen vorgehen, die \"uber die Block-\"ubergreifend g\"ultig sind.}
199 \item\label{conflict} \textbf{nicht zur\"uckgegeben} werden R\"uckgabewerte des Subprogrammes dann, wenn sie im Widerspruch zum ``context'' des aufrunfenden Programmes stehen. Hier ist ein Beispiel:
204 \`$\mathit{(some)}\;\mathit{assumptions}$\\
205 $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
206 \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
207 \>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
208 \>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
209 \>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\
210 \`$x\not=3\land x\not=0$\\
211 \>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
212 \>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
213 \>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
214 \>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
215 \>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
216 \>\>$-6 * x + 5 * x ^ 2 = 0$ \\
217 \>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
218 \>\>$[x = 0, x = \frac{6}{5}]$ \\
219 \`$x = 0\land x = \frac{6}{5}$\\
220 \>$[{x = 0}, x = \frac{6}{5}]$ \\
221 \`{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
222 \>$[x = \frac{6}{5}]$ \\
225 Aufgrund von Punkt.\ref{conflict} oben wird es m\"oglich, aus dem Programm, das obige Rechnung erzeugt, das Statement \textit{Chec\_Elementwise Assumptions} zu streichen:
228 xx\=xx\=xx\=xx\=xx\=xx\=\kill
229 Script Solve\_root\_equation (e\_e::bool) (v\_v::real) = \\
230 \> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@ \\
231 \>\>\> (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\
232 \>\> (L\_L::bool list) = \\
233 \>\>\> (SubProblem (Test', \\
234 \>\>\>\> [linear,univariate,equation,test]\\
235 \>\>\>\> [Test,solve\_linear]) \\
236 \>\>\>\> [BOOL e\_e, REAL v\_v]) \\
237 \> in {Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\
240 Hiermit geht die Entwicklung des Konzeptes von Lucas-Interpretation einen Schritt in die begonnene Richtung weiter, die Verschiebung des Programmieraufwandes von ``computation'' (im herk\"ommlichen programmieren) auf ``deduction'' (im Spezifizieren von Programmeigenschaften) zu unterst\"utzen.
242 \subsection{\"Uberblick: ``contexts'' bei Lucas-Interpretation}
246 \ref{init-ctxt-solve}
248 \ref{init-ctxt-solve}
253 \section{Dokumentation der Meilensteine}Assertions
254 \subsection{Voraussetzungen zum Arbeitsbeginn schaffen}
255 \begin{tabular}[t]{lll}
256 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
257 10.02.2011 & 2:00 & Besprechung der Problemstellung \\
258 11.02.2011 & 1:30 & {\it context}s studieren, Isabelle/Mercurial Installation \\
259 18.02.2011 & 0:15 & meld/tortoisehg installieren \\
260 20.02.2011 & 1:00 & Projektbeschreibung, jedit Probleme \\
261 25.02.2011 & 1:00 & Ausarbeitung Meilensteine \\
262 26.02.2011 & 1:00 & Ausarbeitung Ist-/Soll-Zustand, {\it context}s studieren\\
263 28.02.2011 & 1:15 & Einführungsbeispiel {\it context}s \\
264 28.02.2011 & 1:15 & Projektplan erstellen, formatieren \\
265 01.03.2011 & 1:00 & Projektplan überarbeiten, Stundenlisten \\
268 \subsection{\isac{} auf die letzte Isabelle-Release updaten}
269 Die Arbeit mit den Isabelle {\it context}s wird Anfragen in isabelle-dev@
270 erfordern. isabelle-dev@ beantwortet Fragen i.A. nur für die aktuelle
271 Release. Überraschenderweise wurde vor zwei Wochen eine neue Release
272 veröffentlicht. Daher muss auf diese vor Arbeitsbeginn upgedatet werden.\\
274 \begin{tabular}[t]{lll}
275 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
276 18.02.2011 & 2:45 & Anpassungen an Isabelle2011 \\
277 20.02.2011 & 2:45 & Update auf Isabelle2011, Fehlersuche \\
278 21.02.2011 & 6:30 & ... \\
279 25.02.2011 & 5:30 & ... \\
280 26.02.2011 & 4:30 & ... \\
281 03.03.2011 & 5:00 & ... \\
282 04.03.2011 & 6:00 & Tests reparieren \\
285 \subsection{Parsen aus {\it context}s}
286 Bisher nahm \sisac{} für jede Variable den Typ {\it real} an. Ab jetzt werden Variablen, Terme und Prädikate beim ersten Auftreten im {\it context} eingetragen. User-Input wird mithilfe des {\it context}s typgerecht geparst.\\
288 \begin{tabular}[t]{lll}
289 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
290 02.03.2011 & 1:30 & vorbereitendes Übungsbeispiel \\
291 03.03.2011 & 1:00 & ... \\
292 04.03.2011 & 5:00 & Funktion {\tt parseNEW} schreiben \\
293 05.03.2011 & 3:00 & Funktion {\tt vars} anpassen, {\tt declare\_constraints} neu \\
294 07.03.2011 & 8:45 & {\tt parseNEW}, Spezifikationen studieren \\
295 08.03.2011 & 6:00 & {\it context} in zentrale Datenstrukturen einbauen \\
296 09.03.2011 & 2:00 & Fehlersuche {\it context}-Integration \\
299 \subsection{Spezifikationsphase mit {\it context}s}
300 \sisac{} sah für die Spezifikation eine Datenstruktur vor, die interaktives Spezifizieren effizient unterstützt. Diese Datenstruktur ist nun durch {\it context}s ersetzt. Dadurch ist die bisherige Fixierung auf {\it real} aufgehoben und beliebige Typen werden fehlerfrei behandelt.\\
302 \begin{tabular}[t]{lll}
303 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
304 10.03.2011 & 2:30 & {\it context} in {\tt prep\_ori} und {\tt appl\_add} einbauen\\
305 11.03.2011 & 5:45 & {\tt appl\_add} überarbeiten \\
306 12.03.2011 & 5:15 & Fehlersuche \\
307 14.03.2011 & 2:00 & ... \\
308 16.03.2011 & 2:30 & ... \\
309 17.03.2011 & 1:45 & ... \\
310 18.03.2011 & 4:45 & ..., Optimierung \\
311 19.03.2011 & 5:30 & ... \\
312 21.03.2011 & 3:00 & Abschluss Spezifikationsphase \\
315 \subsection{Lösungsphase mit {\it context}s}
316 Der Lucas-Interpreter hatte Environment und Assertions (precondition, partiality conditions, etc) getrennt gespeichert. Nun sind Environment und Assertions im {\it context} vereint, der Interpreter einfacher und genereller.\\
318 \begin{tabular}[t]{lll}
319 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
320 22.03.2011 & 4:30 & {\it context} in Funktion {\tt solve} einbauen\\
321 23.03.2011 & 4:45 & Tests reparieren \\
322 24.03.2011 & 3:30 & ... \\
323 25.03.2011 & 2:00 & ... \\
324 03.04.2011 & 4:00 & ... \\
325 05.04.2011 & 8:00 & Optimierung \\
326 06.04.2011 & 7:15 & Lösung Exponentenoperator \\
327 07.03.2011 & 7:00 & ... \\
328 12.04.2011 & 3:30 & Projektbericht \\
331 \section{Bericht zum Projektverlauf}
333 \subsection{Voraussetzungen zum Arbeitsbeginn schaffen}
334 Die Größe der Projekte {\it Isabelle} und \sisac{} sowie deren Abgrenzung haben den Weg zu meinem schließlichen Verständnis der Aufgabenstellung etwas langwierig gestaltet. Die lange Vorbereitung hat sich aber positiv auf den weiteren Verlauf des Projektes ausgewirkt.
336 \subsection{\isac{} auf die letzte Isabelle-Release updaten}
337 Da die Veröffentlichung der {\it Isabelle}-Version 2009-2 noch nicht lange zurück lag, kam {\it Isabelle2011} mit vielen grundlegenden Änderungen im System kurz vor Projektbeginn sehr überraschend. Die Mailingliste der Entwickler beantwortet nur Fragen zur aktuellen Release, weshalb ein entsprechendes Update von \sisac{} vor Arbeitsbeginn notwendig war.
338 Dieser Arbeitsschritt beanspruchte wesentlich mehr Zeit als ursprünglich geplant. Als \sisac{} schließlich erfolgreich kompilierte funktionierte eine große Zahl der Tests nicht mehr. Dies machte die selbstständige Arbeit für mich vorerst unmöglich. Ich konnte jedoch in persönlicher Zusammenarbeit mit Walther Neuper meine Fähigkeiten einbringen.
340 \subsection{Parsen aus {\it context}s}
341 In diesem Schritt konnte ich besonders Syntax und Funktionsweise von StandardML, die praktischen, {\it Isabelle}-eigenen Operatoren und die Arbeitsweise mit der Entwicklungsumgebung kennen lernen. Dieser Meilenstein konnte in recht kurzer Zeit abgeschlossen werden.
343 \subsection{Spezifikationsphase mit {\it context}s}
344 Hier konnte ich sehr viel selbstständig arbeiten. Zu Beginn verlief alles völlig problemlos, die Suche nach einem bestimmten Fehler beanspruchte dann aber mit Abstand die meiste Zeit, hatte jedoch zur Folge, dass ich mich sehr intensiv mit dem System auseinandersetzen musste und damit einige Kernfunktionen kennen und verstehen lernte und teilweise sogar etwas optimieren konnte.
345 Insgesamt verlief diese Phase trotz der langwierigen Fehlersuche entsprechend dem Zeitplan.
347 \subsection{Lösungsphase mit {\it context}s}
348 Die Integration von {\it context}s in die Lösungsphase zur Ersetzung und Zusammenführung von Environment und Assertions konnte in enger Zusammenarbeit mit Herrn Neuper fertiggestellt werden. Der Code des Lucas-Interpreters ist jetzt sauberer und die Logik vereinfacht.
351 \section{Abschließende Bemerkungen}
352 Rückblickend betrachte ich das Projektpraktikum als sehr positive Erfahrung, da ich das Gefühl habe, etwas nicht Unwesentliches zur Erweiterung von \sisac{} beigetragen zu haben. Die persönliche Zusammenarbeit mit Akademikern und auch die Verrichtung einer Arbeit, die nach Abschluss gebraucht und verwendet wird, ist eine Erfahrung, die ich im Verlauf meines Studiums leider erst einmal davor machen durfte.\\
353 Der nicht zuletzt durch das überraschend notwendig gewordene Update bedingte zähe Verlauf bis ich endlich wirklich an der eigentlichen Aufgabenstellung arbeiten konnte war etwas ernüchternd, da ich gehofft hatte, das Praktikum bis spätestens Ende März abschließen zu können.\\
354 Die Zusammenarbeit mit Herrn Neuper hat jedenfalls sehr gut funktioniert und aus meiner Sicht haben wir uns sehr gut verstanden. Das hat ein entspanntes Arbeitsklima ermöglicht.
357 \section{Anhang: Demobeispiel}
360 theory All_Ctxt imports Isac begin
362 text {* all changes of context are demonstrated in a mini example.
363 see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 --- *}
365 section {* start of the mini example *}
368 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
370 ("Test", ["sqroot-test","univariate","equation","test"],
371 ["Test","squ-equ-test-subpbl1"]);
372 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
375 section {* start of specify phase *}
377 text {* variables known from formalisation provide type-inference
381 val ctxt = get_ctxt pt p;
382 val SOME known_x = parseNEW ctxt "x + y + z";
383 val SOME unknown = parseNEW ctxt "a + b + c";
387 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
388 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
389 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
390 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
391 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
392 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
393 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
397 section {* start interpretation of method *}
399 text {* preconditions are known at start of interpretation of (root-)method *}
402 get_assumptions_ pt p |> terms2strs;
406 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
407 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
408 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
411 section {* start a subproblem: specification *}
413 text {* variables known from arguments of (sub-)method provide type-inference for further input *}
416 val ctxt = get_ctxt pt p;
417 val SOME known_x = parseNEW ctxt "x+y+z";
418 val SOME unknown = parseNEW ctxt "a+b+c";
422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
423 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
424 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
425 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
426 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
427 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
428 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
429 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
432 section {* interpretation of subproblem's method *}
434 text {* preconds are known at start of interpretation of (sub-)method *}
437 get_assumptions_ pt p |> terms2strs
441 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
445 "artifically inject assumptions";
446 val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
447 val ctxt = insert_assumptions [str2term "x < sub_asm_out",
448 str2term "a < sub_asm_local"] cres;
449 val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
453 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
454 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
457 section {* finish subproblem, return to calling method*}
459 text {* transfer non-local assumptions and result from sub-method to root-method.
460 non-local assumptions are those contaning a variable known in root-method.
464 terms2strs (get_assumptions_ pt p);
468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
472 section {* finish Lucas interpretation *}
474 text {* assumptions collected during lucas-interpretation for proof of postcondition *}
477 terms2strs (get_assumptions_ pt p);