1.1 --- a/doc-src/isac/mlehnfeld/projektbericht.tex Sun May 29 21:02:40 2011 +0200
1.2 +++ b/doc-src/isac/mlehnfeld/projektbericht.tex Mon May 30 02:04:29 2011 +0200
1.3 @@ -42,7 +42,6 @@
1.4 interpretieren, wesentlich erweitern: {\it context}s stellen Isabelles
1.5 automatischen Beweisern die notwendigen Daten bereit.
1.6
1.7 -%\clearpage
1.8
1.9 \section{Planung des Projektes}
1.10 \subsection{Ist-Zustand vor dem Projekt}
1.11 @@ -52,20 +51,23 @@
1.12 \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.
1.13
1.14 \subsection{Zeitplanung f\"ur das Projekt}
1.15 -Die Planung f\"ur das Projekt sah folgende Meilensteine vor:
1.16 +Die Planung f\"ur das Projekt sah folgende Meilensteine vor (Details siehe \ref{ms-desc}):
1.17 \begin{enumerate}
1.18 -\item \textbf{Voraussetzungen zum Arbeitsbeginn schaffen} (10.Feb. -- 28.Feb)\\
1.19 -TODO
1.20 -\item \textbf{\isac{} auf die letzte Isabelle-Release updaten} (TODO)\\
1.21 -TODO
1.22 -\item
1.23 -\item
1.24 +\item \textbf{Voraussetzungen zum Arbeitsbeginn schaffen} (10.02. -- 18.02.)
1.25 + %Beschreibung siehe \ref{ms1_desc}
1.26 +\item \textbf{\isac{} auf die letzte Isabelle-Release updaten} (21.02. -- 25.02.)
1.27 + %Beschreibung siehe \ref{ms2_desc}
1.28 +\item \textbf{Parsen aus \textit{contexts}} (28.02. -- 04.03.)
1.29 + %Beschreibung siehe \ref{ms3_desc}
1.30 +\item \textbf{Spezifikationsphase mit \textit{context}s} (07.03. -- 11.03.)
1.31 + %Beschreibung siehe \ref{ms4_desc}
1.32 +\item \textbf{L\"osungsphase mit \textit{context}s} (14.03. -- 18.03.)
1.33 + %Beschreibung siehe \ref{ms5_desc}
1.34 \end{enumerate}
1.35 -%\clearpage
1.36
1.37 \section{Konzepte und L\"osungen}
1.38 \subsection{Architektur von \isac}
1.39 -Die Grafik auf Seite p.\pageref{architektur} gibt einen \"Uberblick \"uber die Architektur von \sisac:
1.40 +Die Grafik auf Seite \pageref{architektur} gibt einen \"Uberblick \"uber die Architektur von \sisac:
1.41
1.42 \begin{figure} [htb]
1.43 \begin{center}
1.44 @@ -76,20 +78,21 @@
1.45 \end{figure}
1.46 Die Mathematik-Engine von \sisac{} ist nach dem Konzept eines ``Lucas-Interpreters'' (LI) gebaut. Ein LI interpretiert drei Arten von Daten:
1.47 \begin{enumerate}
1.48 -\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.
1.49 -\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.
1.50 -\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.
1.51 +\item\label{spec}\textbf{Spezifikationen}: diese beschreiben ein Problem der angewandten Mathematik durch die Ein- und Ausgabedaten, die ``precondition'' (Pr\"adikate auf den Eingabedaten) und eine ``postcondition'' (eine Relation zwischen Ein- und Ausgabedaten). Spezifikationen stellen den \textit{applikations-orientierten} Aspekt der Mathematik dar.
1.52 +\item \textbf{Programme}: beschreiben den Algorithmus zur L\"osung des spezifizierten Problems. \sisac's Programmsprache ist funktional und hat keine Ein- oder 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.
1.53 +\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 Umfang. Theorien stellen den \textit{deduktiven} Aspekt der Mathematik dar.
1.54 \end{enumerate}
1.55
1.56 -Die Funktionalit\"at eines LI kann in kurzer Form so beschrieben werden \footnote{Siehe http://www.ist.tugraz.at/isac/index.php/Description}:
1.57 +Die Funktionalit\"at eines LI kann in kurzer Form durch die folgenden drei Anspr\"uche erkl\"art werden\footnote{siehe http://www.ist.tugraz.at/isac/index.php/Description}:
1.58 +
1.59 \begin{enumerate}
1.60 -\item
1.61 -\item
1.62 -\item
1.63 +\item \textbf{Benutzereingaben pr\"ufen}: Benutzereingaben sollen so gro\3z\"ugig wie m\"oglich verarbeitet werden. Bei einem gegebenen Problem aus der angewandten Mathematik als formale Spezifikation, wird mit den jeweiligen ``preconditions'' ein ``context'' erzeugt. Nun kann ein Isabelle ``prover'' die Ableitbarkeit einer Benutzereingabe aus dem ``context'' \"uberpr\"ufen. Der ``context'' wird Schritt f\"ur Schritt durch Benutzereingaben erweitert, bis ein Ergebnis vorliegt, das beweisbar die ``postcondition'' aus der Spezifikation erf\"ullt.
1.64 +\item \textbf{Den Benutzer anleiten}: Wei\3 der Lernende nicht mehr weiter, so kann das System den n\"achsten Schritt vorschlagen und den Benutzer so Schritt f\"ur Schritt zum Ergebnis f\"uhren. Ein \sisac{}-Programm wird so interpretiert, wie es bei einem Debugger passiert; die Breakpoints (i.e. Schritte) sind als bestimmte Statements im Programm definiert, die notwendigerweise zum Verlauf der Rechnung bzw. deren Aufbau geh\"oren. An den Breakpoints kann der Benutzer frei entscheiden, ob er den n\"achsten Schritt generieren lassen m\"ochte oder ob er versucht, selbst weiter zu rechnen. Die Herausforderung f\"ur den \textit{Lucas-Interpreter} ist, mit beliebigen Benutzereingaben umgehen zu k\"onnen.
1.65 +\item \textbf{Schritte erkl\"aren}: Bei Interesse hat der Lernende Zugang zu dem Wissen, das f\"ur einen mechanisierten \textit{math assistant} zur L\"osung mathematischer Probleme von N\"oten ist: Definitionen, Axiome und Theoreme (erfasst in ``theories''\footnote{siehe http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index\_thy.html}), Spezifikationen von Problemklassen\footnote{siehe z.B. http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html} und Programme, um die Probleme zu l\"osen\footnote{siehe http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html}. Theoretisch ist dieses Wissen ausreichend, automatisch Erkl\"arungen f\"ur die einzelnen Schritte zu generieren. Das Hintergrundwissen liegt zwar in mathematischer Formulierung vor, es ist jedoch fraglich, wie dies in eine Form gebracht werden kann, die den Lernenden nicht \"uberfordert.
1.66 \end{enumerate}
1.67
1.68 \subsection{Isabelles Konzept von ``contexts''}
1.69 -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:
1.70 +Die Beschreibung dieses bew\"ahrten Konzeptes findet sich in einem internen Papier zur Implementatierung von Isabelles Beweissprache Isar \cite{isar-impl}. Isabelle stellt einen sehr generellen Funktor zur Verf\"ugung:
1.71
1.72 {\tt
1.73 \begin{tabbing}
1.74 @@ -108,7 +111,7 @@
1.75 \>\>\>term -> Proof.context -> Proof.context
1.76 \end{tabbing}
1.77 }
1.78 -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.
1.79 +Das Einzige, was die Definition eines''contexts'' braucht, ist die 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.
1.80
1.81 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:
1.82 {\tt
1.83 @@ -119,7 +122,7 @@
1.84 \>\>\>handle \_ => NONE;
1.85 \end{tabbing}
1.86 }
1.87 -\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}:
1.88 +\textit{Syntax.read\_term ctxt} entnimmt dem ``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} einfach alle unbestimmten Typen auf \textit{real}:
1.89 {\tt
1.90 \begin{tabbing}
1.91 xx\=xx\=xx\=xx\=xx\=\kill
1.92 @@ -132,14 +135,14 @@
1.93 }
1.94
1.95 \subsection{Die Initialisierung von ``contexts''}\label{init-ctxt}
1.96 -``Contexts'' werden anzwei Stellen von Lucas-Interpretation initialisiert: am Beginn der Spezifikations-Phase und zu Beginn der L\"ose-Phase.
1.97 +``Contexts'' werden an zwei Stellen von Lucas-Interpretation initialisiert: am Beginn der Spezifikationsphase und zu Beginn der L\"osungsphase.
1.98
1.99 \begin{enumerate}
1.100 -\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}.
1.101 +\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 mittels \textit{declare\_constraints} mit den Typdeklarationen aller vorkommenden Variablen initialisiert.
1.102
1.103 -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.
1.104 +Im Falle eines Rootproblems kommen die Variablen von einer ``formalization'', einer Kurzbeschreibung der Eingabedaten durch einen Autor. Im Falle eines Subproblems kommen die Variablen von den ``actual arguments'' des Subprogrammes.
1.105
1.106 -\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
1.107 +\item\label{init-ctxt-solve}{Die L\"osungsphase} erzeugt die Rechenschritte aus dem spezifizierten Programm. Zu Beginn der Interpretation des Programmes wird der ``context'' initialisiert mit
1.108 \begin{enumerate}
1.109 \item den Typdeklarationen aller in der Spezifikation vorkommenden Variablen mittels \textit{declare\_constraints}
1.110 \item den ``preconditions'' des (interaktiv oder automatisch) spezifizierten Programmes, genauer: mit den ``preconditions'' des zugeh\"origen Guards, der meist gleich der Spezifikation ist
1.111 @@ -148,9 +151,9 @@
1.112
1.113
1.114 \subsection{Aufbau von ``contexts'' in der Interpretation}\label{partiality}
1.115 -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.
1.116 +W\"ahrend der Interpretation eines Programmes baut der Lucas-Interpreter einen ``context'' auf, indem er alle relevanten ``preconditions'', andere Pr\"adikate -- insbesondere ``partiality conditions'' -- einsammelt. Eine ``partiality condition'' ist zum Beispiel $x\not=0$, die eine Division durch $0$ verhindert.
1.117
1.118 -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~!).
1.119 +Am Ende eines Programmes soll der ``context'' hinreichend logische Information enthalten, sodass Isabelles automatische Beweiser die ``postcondition'' automatisch beweisen k\"onnen (das ist eine k\"unftige Entwicklungsaufgabe!).
1.120
1.121 \subsection{Transfer von ``contexts'' aus Subprogrammen}\label{transfer}
1.122 ``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:
1.123 @@ -170,9 +173,10 @@
1.124 }
1.125 Folgende Daten werden aus dem Sub-``context'' in den ``context'' des aufrufenden Programmes zur\"uckgegeben:
1.126 \begin{enumerate}
1.127 -\item die R\"uckgabewerte des Subprogrammes, soferne sie vom Typ \textit{bool} sind
1.128 -\item alle \textit{assumptions}, die eine Variable enthalten, die auch ein R\"uckgabewerte enth\"alt
1.129 -\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}
1.130 +\item die R\"uckgabewerte des Subprogrammes, sofern sie vom Typ \textit{bool} sind
1.131 +\item alle \textit{assumptions}, die eine Variable enthalten, die auch einer der R\"uckgabewerte enth\"alt
1.132 +\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}
1.133 +\begin{tabbing}
1.134 xxx\=xxx\=\kill
1.135 \`$\mathit{(some)}\;\mathit{assumptions}$\\
1.136 $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
1.137 @@ -195,7 +199,7 @@
1.138 \>$[x = \frac{6}{5}]$ \\
1.139 $[x = \frac{6}{5}]$
1.140 \end{tabbing}
1.141 -der Unterschied begr\"undet sich darin, dass Rechnungen vorzugsweise mit Variablennamen vorgehen, die \"uber die Block-\"ubergreifend g\"ultig sind.}
1.142 +der Unterschied begr\"undet sich darin, dass Rechnungen vorzugsweise mit Variablennamen vorgehen, die block\"ubergreifend g\"ultig sind.
1.143 \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:
1.144 \end{enumerate}
1.145
1.146 @@ -222,7 +226,7 @@
1.147 \>$[x = \frac{6}{5}]$ \\
1.148 $[x = \frac{6}{5}]$
1.149 \end{tabbing}
1.150 -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:
1.151 +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:
1.152 {\tt
1.153 \begin{tabbing}
1.154 xx\=xx\=xx\=xx\=xx\=xx\=\kill
1.155 @@ -234,127 +238,146 @@
1.156 \>\>\>\> [linear,univariate,equation,test]\\
1.157 \>\>\>\> [Test,solve\_linear]) \\
1.158 \>\>\>\> [BOOL e\_e, REAL v\_v]) \\
1.159 -\> in {Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\
1.160 +\> in {Check\_Elementwise L\_L \{(v\_v::real). Assumptions\}})\\
1.161 \end{tabbing}
1.162 }
1.163 -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.
1.164 +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.
1.165
1.166 \subsection{\"Uberblick: ``contexts'' bei Lucas-Interpretation}
1.167 -jedit
1.168
1.169 -\ref{init-ctxt-spec}
1.170 -\ref{init-ctxt-solve}
1.171 -\ref{init-ctxt-spec}
1.172 -\ref{init-ctxt-solve}
1.173 -\ref{partiality}
1.174 -\ref{transfer}
1.175 -\ref{conflict}
1.176 +Im Folgenden betrachten wir ein Bespiel für die Lösung einer Aufgabe durch \sisac. Die gegebenen Codeausschnitte sind nur Teile des gesamten Programmes. Der vollständige Code befindet sich in Anhang \ref{demo-code}.
1.177
1.178 -\section{Dokumentation der Meilensteine}Assertions
1.179 -\subsection{Voraussetzungen zum Arbeitsbeginn schaffen}
1.180 -\begin{tabular}[t]{lll}
1.181 - {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.182 - 10.02.2011 & 2:00 & Besprechung der Problemstellung \\
1.183 - 11.02.2011 & 1:30 & {\it context}s studieren, Isabelle/Mercurial Installation \\
1.184 - 18.02.2011 & 0:15 & meld/tortoisehg installieren \\
1.185 - 20.02.2011 & 1:00 & Projektbeschreibung, jedit Probleme \\
1.186 - 25.02.2011 & 1:00 & Ausarbeitung Meilensteine \\
1.187 - 26.02.2011 & 1:00 & Ausarbeitung Ist-/Soll-Zustand, {\it context}s studieren\\
1.188 - 28.02.2011 & 1:15 & Einführungsbeispiel {\it context}s \\
1.189 - 28.02.2011 & 1:15 & Projektplan erstellen, formatieren \\
1.190 - 01.03.2011 & 1:00 & Projektplan überarbeiten, Stundenlisten \\
1.191 -\end{tabular}
1.192 +\paragraph{Formulierung der Aufgabenstellung und Spezifikation}~\\
1.193
1.194 -\subsection{\isac{} auf die letzte Isabelle-Release updaten}
1.195 +Erklärung siehe \ref{init-ctxt-spec}.
1.196 +\begin{verbatim}
1.197 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
1.198 +val (dI',pI',mI') =
1.199 + ("Test", ["sqroot-test","univariate","equation","test"],
1.200 + ["Test","squ-equ-test-subpbl1"]);
1.201 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.202 +\end{verbatim}
1.203 +\textit{fmz} enthält also die zwei Eingabegrößen und die gesuchte Ausgabegröße, also die Liste aller Lösungen für \textit{x} in der Gleichung $x + 1 = 2$. Die zweite Zeile definiert den Namen der ``theory'' mit dem deduktiven Hintergrundwissen, die Spezifikation in Form einer Liste und das zu verwendende Programm.\\
1.204 +\textit{CalcTreeTEST} erzeugt schlie\3lich die grundlegenden Datenstrukturen für die folgenden Berechnungen. Beispielsweise wird ein ``context'' erzeugt, der nun im Baum \textit{pt} an der Position \textit{p} steht.
1.205 +\begin{verbatim}
1.206 +val ctxt = get_ctxt pt p;
1.207 +val SOME known_x = parseNEW ctxt "x + y + z";
1.208 +val SOME unknown = parseNEW ctxt "a + b + c";
1.209 +\end{verbatim}
1.210 +Dies erzeugt folgenden Output:
1.211 +\begin{verbatim}
1.212 +val ctxt = <context>: Proof.context
1.213 +val known_x =
1.214 + Const ("Groups.plus_class.plus",
1.215 + "RealDef.real => RealDef.real => RealDef.real") $
1.216 + (Const ("Groups.plus_class.plus",
1.217 + "RealDef.real => RealDef.real => RealDef.real") $
1.218 + Free ("x", "RealDef.real") $ Free ("y", "RealDef.real")) $
1.219 + Free ("z", "RealDef.real"):
1.220 + term
1.221 +val unknown =
1.222 + Const ("Groups.plus_class.plus", "'a => 'a => 'a") $
1.223 + (Const ("Groups.plus_class.plus", "'a => 'a => 'a")
1.224 + $ Free ("a", "'a") $ Free ("b", "'a")) $
1.225 + Free ("c", "'a"):
1.226 + term
1.227 +\end{verbatim}
1.228 +Der Output dieser Zeilen zeigt die neue Funktionalität anhand der Erkennung des Typs \textit{real} für die Variablen \textit{x}, \textit{y} und \textit{z} mittels Typinferenz, im Gegensatz zu den Unbekannten \textit{a}, \textit{b} und \textit{c} (unbekannter Typ \textit{'a}.
1.229 +
1.230 +\paragraph{Beginn der Interpretation}~\\
1.231 +
1.232 +Nach einigen Schritten der Mathematik-Engine ist die Spezifikationsphase beendet und die Interpretation des Programmes kann beginnen. Die ``precondition'' ist in den Assumptions enthalten:
1.233 +\begin{verbatim}
1.234 +get_assumptions_ pt p |> terms2strs
1.235 +\end{verbatim}
1.236 +Output:
1.237 +\begin{verbatim}
1.238 +val it = ["precond_rootmet x"]: string list
1.239 +\end{verbatim}
1.240 +
1.241 +\paragraph{Bearbeitung eines Subproblems}~\\
1.242 +
1.243 +Einige Ausführungsschritte später startet der Interpreter mit der Gleichung $-1 + x = 0$ ein Subproblem, beginnt dort wiederum mit Spezifikationsphase und setzt mit der Lösungsphase fort.\\
1.244 +In einem Zwischenschritt bestehen die lokalen Assumptions aus der Annahme, dass die Gleichung mit der Gleichheitsregel zu matchen ist:\\
1.245 +\begin{verbatim}
1.246 +["matches (?a = ?b) (-1 + x = 0)"]: string list
1.247 +\end{verbatim}
1.248 +Nach künstlichem Einfügen zweier Assumptions und Beendigung des Subproblems steht eine Lösung für \textit{x} in den Assumptions:\\
1.249 +\texttt{[\dq{}matches (?a = ?b) (-1 + x = 0)\dq{}, \dq{}x < sub\_asm\_out\dq{}, \dq{}{\bf x = 1}\dq{}, \dq{}precond\_rootmet x\dq{}]: string list}\\
1.250 +\\
1.251 +Bei der Rückkehr aus dem Subproblem könnte eine erzeugte Lösung aufgrund einer Bedingungsverletzung wieder wegfallen, hier ist das nicht der Fall. Die Überprüfung dieser Bedingungen (siehe \ref{partiality}) geschieht beim Transfer des lokalen ``contexts'' in den übergeordneten (hier der des Rootproblems, siehe \ref{transfer}).
1.252 +
1.253 +\paragraph{Abschluss der Berechnung}~\\
1.254 +
1.255 +Nach den letzten Aufrufen der Mathematik-Engine stehen alle Schritte fest:
1.256 +\begin{verbatim}[
1.257 +(([], Frm), solve (x + 1 = 2, x)),
1.258 +(([1], Frm), x + 1 = 2),
1.259 +(([1], Res), x + 1 + -1 * 2 = 0),
1.260 +(([2], Res), -1 + x = 0),
1.261 +(([3], Pbl), solve (-1 + x = 0, x)),
1.262 +(([3,1], Frm), -1 + x = 0),
1.263 +(([3,1], Res), x = 0 + -1 * -1),
1.264 +(([3,2], Res), x = 1),
1.265 +(([3], Res), [x = 1]),
1.266 +(([4], Res), [x = 1]),
1.267 +(([], Res), [x = 1])]
1.268 +\end{verbatim}
1.269 +
1.270 +\section{Beschreibung der Meilensteine}\label{ms-desc}
1.271 +\subsection{Voraussetzungen zum Arbeitsbeginn schaffen}\label{ms1_desc}
1.272 +Die Komplexit\"at \sisac{}s, welches auf Konzepten von Isabelle aufbaut und die tief ins System eingreifenden Ver\"anderungen in den bevorstehenden Meilensteinen machen eine intensive Auseinandersetzung mit Isabelle, insbesondere mit dem Konzept der ``contexts'', und dem \sisac-Code notwendig. Darunter fallen neben dem Lesen von Dokumentationen auch die gezielte Suche von Anwendungsf\"allen im bestehenden Code, sowie das Studieren von Coding Standards und ein Vertrautmachen mit den im \sisac-Team \"ublichen Workflows.
1.273 +
1.274 +\subsection{\isac{} auf die letzte Isabelle-Release updaten}\label{ms2_desc}
1.275 Die Arbeit mit den Isabelle {\it context}s wird Anfragen in isabelle-dev@
1.276 -erfordern. isabelle-dev@ beantwortet Fragen i.A. nur für die aktuelle
1.277 -Release. Überraschenderweise wurde vor zwei Wochen eine neue Release
1.278 -veröffentlicht. Daher muss auf diese vor Arbeitsbeginn upgedatet werden.\\
1.279 -\\
1.280 -\begin{tabular}[t]{lll}
1.281 - {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.282 - 18.02.2011 & 2:45 & Anpassungen an Isabelle2011 \\
1.283 - 20.02.2011 & 2:45 & Update auf Isabelle2011, Fehlersuche \\
1.284 - 21.02.2011 & 6:30 & ... \\
1.285 - 25.02.2011 & 5:30 & ... \\
1.286 - 26.02.2011 & 4:30 & ... \\
1.287 - 03.03.2011 & 5:00 & ... \\
1.288 - 04.03.2011 & 6:00 & Tests reparieren \\
1.289 -\end{tabular}
1.290 +erfordern. isabelle-dev@ beantwortet Fragen i.A. nur f\"ur die aktuelle
1.291 +Release. Überraschenderweise wurde zwei Wochen vor Beginn des Projektpraktikums eine neue Release
1.292 +veröffentlicht. Daher muss auf diese vor Arbeitsbeginn upgedatet werden.
1.293
1.294 -\subsection{Parsen aus {\it context}s}
1.295 -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.\\
1.296 -\\
1.297 -\begin{tabular}[t]{lll}
1.298 - {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.299 - 02.03.2011 & 1:30 & vorbereitendes Übungsbeispiel \\
1.300 - 03.03.2011 & 1:00 & ... \\
1.301 - 04.03.2011 & 5:00 & Funktion {\tt parseNEW} schreiben \\
1.302 - 05.03.2011 & 3:00 & Funktion {\tt vars} anpassen, {\tt declare\_constraints} neu \\
1.303 - 07.03.2011 & 8:45 & {\tt parseNEW}, Spezifikationen studieren \\
1.304 - 08.03.2011 & 6:00 & {\it context} in zentrale Datenstrukturen einbauen \\
1.305 - 09.03.2011 & 2:00 & Fehlersuche {\it context}-Integration \\
1.306 -\end{tabular}
1.307 +\subsection{Parsen aus {\it context}s}\label{ms3_desc}
1.308 +Bisher nahm \sisac{} für jede Variable den Typ {\it real} an. Variablen, Terme und Pr\"adikate sollen nun beim ersten Auftreten im {\it context} eingetragen werden. User-Input wird mithilfe des {\it context}s mittels Typinferenz typgerecht geparst. Die Verwendungen der bestehenden \textit{parse}-Funktion m\"ussen im ganzen System ersetzt und angepasst werden.
1.309
1.310 -\subsection{Spezifikationsphase mit {\it context}s}
1.311 -\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.\\
1.312 -\\
1.313 -\begin{tabular}[t]{lll}
1.314 - {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.315 - 10.03.2011 & 2:30 & {\it context} in {\tt prep\_ori} und {\tt appl\_add} einbauen\\
1.316 - 11.03.2011 & 5:45 & {\tt appl\_add} überarbeiten \\
1.317 - 12.03.2011 & 5:15 & Fehlersuche \\
1.318 - 14.03.2011 & 2:00 & ... \\
1.319 - 16.03.2011 & 2:30 & ... \\
1.320 - 17.03.2011 & 1:45 & ... \\
1.321 - 18.03.2011 & 4:45 & ..., Optimierung \\
1.322 - 19.03.2011 & 5:30 & ... \\
1.323 - 21.03.2011 & 3:00 & Abschluss Spezifikationsphase \\
1.324 -\end{tabular}
1.325 +\subsection{Spezifikationsphase mit {\it context}s}\label{ms4_desc}
1.326 +\sisac{} sah für die Spezifikation eine Datenstruktur vor, die interaktives Spezifizieren effizient unterstützt. Diese Datenstruktur soll nun durch {\it context}s ersetzt werden. Dadurch ist die bisherige Fixierung auf {\it real} aufgehoben und beliebige Typen werden fehlerfrei behandelt. Dieser Schritt macht weitere Eingriffe in grundlegende Funktionen und Datenstrukturen des Systems notwendig.
1.327
1.328 -\subsection{Lösungsphase mit {\it context}s}
1.329 -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.\\
1.330 -\\
1.331 -\begin{tabular}[t]{lll}
1.332 - {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.333 - 22.03.2011 & 4:30 & {\it context} in Funktion {\tt solve} einbauen\\
1.334 - 23.03.2011 & 4:45 & Tests reparieren \\
1.335 - 24.03.2011 & 3:30 & ... \\
1.336 - 25.03.2011 & 2:00 & ... \\
1.337 - 03.04.2011 & 4:00 & ... \\
1.338 - 05.04.2011 & 8:00 & Optimierung \\
1.339 - 06.04.2011 & 7:15 & Lösung Exponentenoperator \\
1.340 - 07.03.2011 & 7:00 & ... \\
1.341 - 12.04.2011 & 3:30 & Projektbericht \\
1.342 -\end{tabular}
1.343 +\subsection{L\"osungsphase mit {\it context}s}\label{ms5_desc}
1.344 +Der Lucas-Interpreter speicherte Assumptions (precondition, partiality conditions, etc.) in einer eigenen Datenstruktur im Rechenbaum. Nun sollen Assumptions im {\it context} verwaltet werden. Dazu sind Schreib- und Lesefunktionen zu implementieren und alle Verwendungen von Assumptions entsprechend anzupassen.
1.345
1.346 \section{Bericht zum Projektverlauf}
1.347
1.348 \subsection{Voraussetzungen zum Arbeitsbeginn schaffen}
1.349 -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.
1.350 +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. Dazu kamen nicht geplante, organisatorische Vorbereitungen, wie die Erstellung einer Projektbeschreibung und des -planes. Die lange Vorbereitung hat sich aber positiv auf den weiteren Verlauf des Projektes ausgewirkt.
1.351
1.352 \subsection{\isac{} auf die letzte Isabelle-Release updaten}
1.353 -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.
1.354 -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.
1.355 +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.\\
1.356 +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. Die Notwendigkeit dieser persönlichen Zusammenarbeit verzögerte den Projektverlauf.
1.357
1.358 \subsection{Parsen aus {\it context}s}
1.359 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.
1.360
1.361 \subsection{Spezifikationsphase mit {\it context}s}
1.362 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.
1.363 -Insgesamt verlief diese Phase trotz der langwierigen Fehlersuche entsprechend dem Zeitplan.
1.364 +Insgesamt verlief diese Phase trotz der langwierigen Fehlersuche nicht viel langsamer als geplant.
1.365
1.366 -\subsection{Lösungsphase mit {\it context}s}
1.367 -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.
1.368 +\subsection{L\"osungsphase mit {\it context}s}
1.369 +Die Integration von {\it context}s in die Lösungsphase zur Ersetzung der ursprünglichen behandlung von Assertions konnte in enger Zusammenarbeit mit Herrn Neuper fertiggestellt werden, persönliche Termine auf beiden Seiten verlängerten aber den zeitlichen Verlauf. Der Code des Lucas-Interpreters ist jetzt sauberer und die Logik vereinfacht.
1.370
1.371
1.372 \section{Abschließende Bemerkungen}
1.373 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.\\
1.374 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.\\
1.375 -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.
1.376 +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.\\
1.377 +Da mir bis zum Abschluss meiner Arbeit nicht bewusst war, dass eine Präsentation zu halten und ein umfangreicher Projektbericht abzufassen sind, musste ich den für eine Lehrveranstaltung von 6 ECTS vorgesehenen Arbeitsaufwand deutlich überschreiten. Das und die zeitliche Verzögerung des Projektes geben der Freude über den erfolgreichen Abschluss der geplanten Aufgaben und deren interessanten Charakter einen bitteren Beigeschmack.
1.378
1.379 +\clearpage
1.380 +
1.381 +\bibliography{bib}
1.382 +
1.383 +\clearpage
1.384 +
1.385 +\appendix
1.386 %\section*{Anhang}
1.387 -\section{Anhang: Demobeispiel}
1.388 +\section{Demobeispiel}\label{demo-code}
1.389 \begin{verbatim}
1.390
1.391 theory All_Ctxt imports Isac begin
1.392 @@ -396,7 +419,8 @@
1.393
1.394 section {* start interpretation of method *}
1.395
1.396 -text {* preconditions are known at start of interpretation of (root-)method *}
1.397 +text {* preconditions are known at start of
1.398 + interpretation of (root-)method *}
1.399
1.400 ML {*
1.401 get_assumptions_ pt p |> terms2strs;
1.402 @@ -410,7 +434,8 @@
1.403
1.404 section {* start a subproblem: specification *}
1.405
1.406 -text {* variables known from arguments of (sub-)method provide type-inference for further input *}
1.407 +text {* variables known from arguments of (sub-)method
1.408 + provide type-inference for further input *}
1.409
1.410 ML {*
1.411 val ctxt = get_ctxt pt p;
1.412 @@ -456,8 +481,10 @@
1.413
1.414 section {* finish subproblem, return to calling method*}
1.415
1.416 -text {* transfer non-local assumptions and result from sub-method to root-method.
1.417 - non-local assumptions are those contaning a variable known in root-method.
1.418 +text {* transfer non-local assumptions and result from sub-method
1.419 + to root-method.
1.420 + non-local assumptions are those contaning a variable known
1.421 + in root-method.
1.422 *}
1.423
1.424 ML {*
1.425 @@ -471,7 +498,8 @@
1.426
1.427 section {* finish Lucas interpretation *}
1.428
1.429 -text {* assumptions collected during lucas-interpretation for proof of postcondition *}
1.430 +text {* assumptions collected during lucas-interpretation
1.431 + for proof of postcondition *}
1.432
1.433 ML {*
1.434 terms2strs (get_assumptions_ pt p);
1.435 @@ -484,5 +512,72 @@
1.436 end
1.437 \end{verbatim}
1.438
1.439 -\bibliography{bib}
1.440 +\section{Stundenliste}
1.441 +
1.442 +\subsection*{Voraussetzungen zum Arbeitsbeginn schaffen}
1.443 +\begin{tabular}[t]{lll}
1.444 + {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.445 + 10.02.2011 & 2:00 & Besprechung der Problemstellung \\
1.446 + 11.02.2011 & 1:30 & {\it context}s studieren, Isabelle/Mercurial Installation \\
1.447 + 18.02.2011 & 0:15 & meld/tortoisehg installieren \\
1.448 + 20.02.2011 & 1:00 & Projektbeschreibung, jedit Probleme \\
1.449 + 25.02.2011 & 1:00 & Ausarbeitung Meilensteine \\
1.450 + 26.02.2011 & 1:00 & Ausarbeitung Ist-/Soll-Zustand, {\it context}s studieren\\
1.451 + 28.02.2011 & 1:15 & Einführungsbeispiel {\it context}s \\
1.452 + 28.02.2011 & 1:15 & Projektplan erstellen, formatieren \\
1.453 + 01.03.2011 & 1:00 & Projektplan überarbeiten, Stundenlisten \\
1.454 +\end{tabular}
1.455 +
1.456 +\subsection*{\isac{} auf die letzte Isabelle-Release updaten}
1.457 +\begin{tabular}[t]{lll}
1.458 + {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.459 + 18.02.2011 & 2:45 & Anpassungen an Isabelle2011 \\
1.460 + 20.02.2011 & 2:45 & Update auf Isabelle2011, Fehlersuche \\
1.461 + 21.02.2011 & 6:30 & ... \\
1.462 + 25.02.2011 & 5:30 & ... \\
1.463 + 26.02.2011 & 4:30 & ... \\
1.464 + 03.03.2011 & 5:00 & ... \\
1.465 + 04.03.2011 & 6:00 & Tests reparieren \\
1.466 +\end{tabular}
1.467 +
1.468 +\subsection*{Parsen aus \textit{contexts}}
1.469 +\begin{tabular}[t]{lll}
1.470 + {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.471 + 02.03.2011 & 1:30 & vorbereitendes Übungsbeispiel \\
1.472 + 03.03.2011 & 1:00 & ... \\
1.473 + 04.03.2011 & 5:00 & Funktion {\tt parseNEW} schreiben \\
1.474 + 05.03.2011 & 3:00 & Funktion {\tt vars} anpassen, {\tt declare\_constraints} neu \\
1.475 + 07.03.2011 & 8:45 & {\tt parseNEW}, Spezifikationen studieren \\
1.476 + 08.03.2011 & 6:00 & {\it context} in zentrale Datenstrukturen einbauen \\
1.477 + 09.03.2011 & 2:00 & Fehlersuche {\it context}-Integration \\
1.478 +\end{tabular}
1.479 +
1.480 +\subsection*{Spezifikationsphase mit \textit{context}s}
1.481 +\begin{tabular}[t]{lll}
1.482 + {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.483 + 10.03.2011 & 2:30 & {\it context} in {\tt prep\_ori} und {\tt appl\_add} einbauen\\
1.484 + 11.03.2011 & 5:45 & {\tt appl\_add} überarbeiten \\
1.485 + 12.03.2011 & 5:15 & Fehlersuche \\
1.486 + 14.03.2011 & 2:00 & ... \\
1.487 + 16.03.2011 & 2:30 & ... \\
1.488 + 17.03.2011 & 1:45 & ... \\
1.489 + 18.03.2011 & 4:45 & ..., Optimierung \\
1.490 + 19.03.2011 & 5:30 & ... \\
1.491 + 21.03.2011 & 3:00 & Abschluss Spezifikationsphase \\
1.492 +\end{tabular}
1.493 +
1.494 +\subsection*{L\"osungsphase mit \textit{context}s}
1.495 +\begin{tabular}[t]{lll}
1.496 + {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.497 + 22.03.2011 & 4:30 & {\it context} in Funktion {\tt solve} einbauen\\
1.498 + 23.03.2011 & 4:45 & Tests reparieren \\
1.499 + 24.03.2011 & 3:30 & ... \\
1.500 + 25.03.2011 & 2:00 & ... \\
1.501 + 03.04.2011 & 4:00 & ... \\
1.502 + 05.04.2011 & 8:00 & Optimierung \\
1.503 + 06.04.2011 & 7:15 & L\"osung Exponentenoperator \\
1.504 + 07.04.2011 & 7:00 & ... \\
1.505 + 12.04.2011 & 3:30 & Projektbericht \\
1.506 +\end{tabular}
1.507 +
1.508 \end{document}