1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/mlehnfeld/bib.bib Sun May 29 21:02:40 2011 +0200
1.3 @@ -0,0 +1,26 @@
1.4 +@Book{Nipkow-Paulson-Wenzel:2002,
1.5 + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
1.6 + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
1.7 + publisher = {Springer},
1.8 + series = {LNCS},
1.9 + volume = 2283,
1.10 + year = 2002}
1.11 +
1.12 +@Article{plmms10,
1.13 + author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
1.14 + title = {{CTP}-based programming languages~? Considerations about an experimental design},
1.15 + journal = {ACM Communications in Computer Algebra},
1.16 + year = {2010},
1.17 + volume = {44},
1.18 + number = {1/2},
1.19 + pages = {27-41},
1.20 + doi = {10.1145/1838599.1838621}
1.21 +}
1.22 +
1.23 +@Manual{isar-impl,
1.24 + title = {The {Isabelle/Isar} Implementation},
1.25 + author = {Makarius Wenzel},
1.26 + month = {30 January},
1.27 + year = {2011},
1.28 + note = {With contributions by Florian Haftmann and Larry Paulson}
1.29 +}
2.1 --- a/doc-src/isac/mlehnfeld/projektbericht.tex Sun May 29 18:21:04 2011 +0200
2.2 +++ b/doc-src/isac/mlehnfeld/projektbericht.tex Sun May 29 21:02:40 2011 +0200
2.3 @@ -1,7 +1,10 @@
2.4 \documentclass[a4paper,12pt]{article}
2.5 -
2.6 +%
2.7 \usepackage[ngerman]{babel}
2.8 \usepackage[utf8]{inputenc}
2.9 +\usepackage{ngerman}
2.10 +\usepackage{graphicx}
2.11 +\bibliographystyle{alpha}
2.12
2.13 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
2.14 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
2.15 @@ -13,7 +16,8 @@
2.16 \author{Mathias Lehnfeld\\
2.17 {\tt mathias.lehnfeld@gmx.at}}
2.18 \maketitle
2.19 -
2.20 +\clearpage
2.21 +\tableofcontents
2.22 \clearpage
2.23
2.24
2.25 @@ -38,19 +42,215 @@
2.26 interpretieren, wesentlich erweitern: {\it context}s stellen Isabelles
2.27 automatischen Beweisern die notwendigen Daten bereit.
2.28
2.29 -\clearpage
2.30 +%\clearpage
2.31
2.32 -\section{Planung des Projektinhaltes}
2.33 +\section{Planung des Projektes}
2.34 \subsection{Ist-Zustand vor dem Projekt}
2.35 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.
2.36
2.37 \subsection{Geplanter Soll-Zustand nach dem Projekt}
2.38 \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.
2.39
2.40 -\clearpage
2.41 +\subsection{Zeitplanung f\"ur das Projekt}
2.42 +Die Planung f\"ur das Projekt sah folgende Meilensteine vor:
2.43 +\begin{enumerate}
2.44 +\item \textbf{Voraussetzungen zum Arbeitsbeginn schaffen} (10.Feb. -- 28.Feb)\\
2.45 +TODO
2.46 +\item \textbf{\isac{} auf die letzte Isabelle-Release updaten} (TODO)\\
2.47 +TODO
2.48 +\item
2.49 +\item
2.50 +\end{enumerate}
2.51 +%\clearpage
2.52
2.53 -\section{Dokumentation der Meilensteine}
2.54 +\section{Konzepte und L\"osungen}
2.55 +\subsection{Architektur von \isac}
2.56 +Die Grafik auf Seite p.\pageref{architektur} gibt einen \"Uberblick \"uber die Architektur von \sisac:
2.57
2.58 +\begin{figure} [htb]
2.59 +\begin{center}
2.60 + \includegraphics[width=120mm]{overview.pdf}
2.61 +\end{center}
2.62 +\caption{Lucas-interpreter und Isabelle}
2.63 +\label{architektur}
2.64 +\end{figure}
2.65 +Die Mathematik-Engine von \sisac{} ist nach dem Konzept eines ``Lucas-Interpreters'' (LI) gebaut. Ein LI interpretiert drei Arten von Daten:
2.66 +\begin{enumerate}
2.67 +\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.
2.68 +\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.
2.69 +\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.
2.70 +\end{enumerate}
2.71 +
2.72 +Die Funktionalit\"at eines LI kann in kurzer Form so beschrieben werden \footnote{Siehe http://www.ist.tugraz.at/isac/index.php/Description}:
2.73 +\begin{enumerate}
2.74 +\item
2.75 +\item
2.76 +\item
2.77 +\end{enumerate}
2.78 +
2.79 +\subsection{Isabelles Konzept von ``contexts''}
2.80 +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:
2.81 +
2.82 +{\tt
2.83 +\begin{tabbing}
2.84 +xx\=xx\=in\=\kill
2.85 +structure ContextData = {Proof\_Data}\\
2.86 +\>~({type T} = term list\\
2.87 +\>\>{fun init \_} = []);\\
2.88 +\\
2.89 +fun insert\_assumptions asms = \\
2.90 +\>\>\>ContextData{.map} (fn xs => distinct (data@xs));\\
2.91 +\\
2.92 +fun get\_assumptions ctxt = ContextData{.get} ctxt;\\
2.93 +\\
2.94 +\\
2.95 +val declare\_constraints : \\
2.96 +\>\>\>term -> Proof.context -> Proof.context
2.97 +\end{tabbing}
2.98 +}
2.99 +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.
2.100 +
2.101 +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:
2.102 +{\tt
2.103 +\begin{tabbing}
2.104 +xx\=xx\=xx\=xx\=xx\=\kill
2.105 +fun parseNEW ctxt str = \\
2.106 +\>\>\>SOME ({Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
2.107 +\>\>\>handle \_ => NONE;
2.108 + \end{tabbing}
2.109 +}
2.110 +\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}:
2.111 +{\tt
2.112 +\begin{tabbing}
2.113 +xx\=xx\=xx\=xx\=xx\=\kill
2.114 +fun parse thy str =\\
2.115 +\>(let val t = ({typ\_a2real} o numbers\_to\_string)\\
2.116 +\>\>\>\>({Syntax.read\_term\_global thy} str)\\
2.117 +\>\>in SOME (cterm\_of thy t) end)\\
2.118 +\>\>\>handle \_ => NONE;\\
2.119 + \end{tabbing}
2.120 +}
2.121 +
2.122 +\subsection{Die Initialisierung von ``contexts''}\label{init-ctxt}
2.123 +``Contexts'' werden anzwei Stellen von Lucas-Interpretation initialisiert: am Beginn der Spezifikations-Phase und zu Beginn der L\"ose-Phase.
2.124 +
2.125 +\begin{enumerate}
2.126 +\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}.
2.127 +
2.128 +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.
2.129 +
2.130 +\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
2.131 + \begin{enumerate}
2.132 + \item den Typdeklarationen aller in der Spezifikation vorkommenden Variablen mittels \textit{declare\_constraints}
2.133 + \item den ``preconditions'' des (interaktiv oder automatisch) spezifizierten Programmes, genauer: mit den ``preconditions'' des zugeh\"origen Guards, der meist gleich der Spezifikation ist
2.134 + \end{enumerate}
2.135 +\end{enumerate}
2.136 +
2.137 +
2.138 +\subsection{Aufbau von ``contexts'' in der Interpretation}\label{partiality}
2.139 +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.
2.140 +
2.141 +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~!).
2.142 +
2.143 +\subsection{Transfer von ``contexts'' aus Subprogrammen}\label{transfer}
2.144 +``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:
2.145 +{\tt
2.146 +\begin{tabbing}
2.147 +xx\=xx\=xx\=xx\=xx\=\kill
2.148 +fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\
2.149 +\> let\\
2.150 +\>\> val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\
2.151 +\>\> fun transfer [] to\_ctxt = to\_ctxt\\
2.152 +\>\>\> | transfer (from\_asm::fas) to\_ctxt =\\
2.153 +\>\>\>\>\> if inter op = (vars from\_asm) to\_vars = []\\
2.154 +\>\>\>\>\> then transfer fas to\_ctxt\\
2.155 +\>\>\>\>\> else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\
2.156 +\> in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\
2.157 + \end{tabbing}
2.158 +}
2.159 +Folgende Daten werden aus dem Sub-``context'' in den ``context'' des aufrufenden Programmes zur\"uckgegeben:
2.160 +\begin{enumerate}
2.161 +\item die R\"uckgabewerte des Subprogrammes, soferne sie vom Typ \textit{bool} sind
2.162 +\item alle \textit{assumptions}, die eine Variable enthalten, die auch ein R\"uckgabewerte enth\"alt
2.163 +\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}
2.164 +xxx\=xxx\=\kill
2.165 + \`$\mathit{(some)}\;\mathit{assumptions}$\\
2.166 +$\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
2.167 +% \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
2.168 +%\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
2.169 +%\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
2.170 +\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\
2.171 + \`$x\not=3\land x\not=0$\\
2.172 +\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
2.173 +\>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
2.174 +%\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
2.175 +%\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
2.176 +\>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
2.177 +\>\>$-6 * x + 5 * x ^ 2 = 0$ \\
2.178 +\>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
2.179 +\>\>$[x = 0, x = \frac{6}{5}]$ \\
2.180 + \`$x = 0\land x = \frac{6}{5}$\\
2.181 +\>$[{x = 0}, x = \frac{6}{5}]$ \\
2.182 + \`{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
2.183 +\>$[x = \frac{6}{5}]$ \\
2.184 +$[x = \frac{6}{5}]$
2.185 +\end{tabbing}
2.186 +der Unterschied begr\"undet sich darin, dass Rechnungen vorzugsweise mit Variablennamen vorgehen, die \"uber die Block-\"ubergreifend g\"ultig sind.}
2.187 +\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:
2.188 +\end{enumerate}
2.189 +
2.190 +\begin{tabbing}
2.191 +xxx\=xxx\=\kill
2.192 + \`$\mathit{(some)}\;\mathit{assumptions}$\\
2.193 +$\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
2.194 + \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
2.195 +\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
2.196 +\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
2.197 +\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\
2.198 + \`$x\not=3\land x\not=0$\\
2.199 +\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
2.200 +\>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
2.201 +\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
2.202 +\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
2.203 +\>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
2.204 +\>\>$-6 * x + 5 * x ^ 2 = 0$ \\
2.205 +\>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
2.206 +\>\>$[x = 0, x = \frac{6}{5}]$ \\
2.207 + \`$x = 0\land x = \frac{6}{5}$\\
2.208 +\>$[{x = 0}, x = \frac{6}{5}]$ \\
2.209 + \`{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
2.210 +\>$[x = \frac{6}{5}]$ \\
2.211 +$[x = \frac{6}{5}]$
2.212 +\end{tabbing}
2.213 +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:
2.214 +{\tt
2.215 +\begin{tabbing}
2.216 +xx\=xx\=xx\=xx\=xx\=xx\=\kill
2.217 +Script Solve\_root\_equation (e\_e::bool) (v\_v::real) = \\
2.218 +\> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@ \\
2.219 +\>\>\> (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\
2.220 +\>\> (L\_L::bool list) = \\
2.221 +\>\>\> (SubProblem (Test', \\
2.222 +\>\>\>\> [linear,univariate,equation,test]\\
2.223 +\>\>\>\> [Test,solve\_linear]) \\
2.224 +\>\>\>\> [BOOL e\_e, REAL v\_v]) \\
2.225 +\> in {Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\
2.226 +\end{tabbing}
2.227 +}
2.228 +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.
2.229 +
2.230 +\subsection{\"Uberblick: ``contexts'' bei Lucas-Interpretation}
2.231 +jedit
2.232 +
2.233 +\ref{init-ctxt-spec}
2.234 +\ref{init-ctxt-solve}
2.235 +\ref{init-ctxt-spec}
2.236 +\ref{init-ctxt-solve}
2.237 +\ref{partiality}
2.238 +\ref{transfer}
2.239 +\ref{conflict}
2.240 +
2.241 +\section{Dokumentation der Meilensteine}Assertions
2.242 \subsection{Voraussetzungen zum Arbeitsbeginn schaffen}
2.243 \begin{tabular}[t]{lll}
2.244 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
2.245 @@ -153,4 +353,136 @@
2.246 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.\\
2.247 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.
2.248
2.249 +%\section*{Anhang}
2.250 +\section{Anhang: Demobeispiel}
2.251 +\begin{verbatim}
2.252 +
2.253 +theory All_Ctxt imports Isac begin
2.254 +
2.255 +text {* all changes of context are demonstrated in a mini example.
2.256 + see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 --- *}
2.257 +
2.258 +section {* start of the mini example *}
2.259 +
2.260 +ML {*
2.261 + val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
2.262 + val (dI',pI',mI') =
2.263 + ("Test", ["sqroot-test","univariate","equation","test"],
2.264 + ["Test","squ-equ-test-subpbl1"]);
2.265 + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.266 +*}
2.267 +
2.268 +section {* start of specify phase *}
2.269 +
2.270 +text {* variables known from formalisation provide type-inference
2.271 + for further input *}
2.272 +
2.273 +ML {*
2.274 + val ctxt = get_ctxt pt p;
2.275 + val SOME known_x = parseNEW ctxt "x + y + z";
2.276 + val SOME unknown = parseNEW ctxt "a + b + c";
2.277 +*}
2.278 +
2.279 +ML {*
2.280 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.281 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.282 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.283 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.284 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.285 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.286 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.287 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.288 +*}
2.289 +
2.290 +section {* start interpretation of method *}
2.291 +
2.292 +text {* preconditions are known at start of interpretation of (root-)method *}
2.293 +
2.294 +ML {*
2.295 + get_assumptions_ pt p |> terms2strs;
2.296 +*}
2.297 +
2.298 +ML {*
2.299 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.300 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.301 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.302 +*}
2.303 +
2.304 +section {* start a subproblem: specification *}
2.305 +
2.306 +text {* variables known from arguments of (sub-)method provide type-inference for further input *}
2.307 +
2.308 +ML {*
2.309 + val ctxt = get_ctxt pt p;
2.310 + val SOME known_x = parseNEW ctxt "x+y+z";
2.311 + val SOME unknown = parseNEW ctxt "a+b+c";
2.312 +*}
2.313 +
2.314 +ML {*
2.315 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.316 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.317 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.318 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.319 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.320 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.321 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.322 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.323 +*}
2.324 +
2.325 +section {* interpretation of subproblem's method *}
2.326 +
2.327 +text {* preconds are known at start of interpretation of (sub-)method *}
2.328 +
2.329 +ML {*
2.330 + get_assumptions_ pt p |> terms2strs
2.331 +*}
2.332 +
2.333 +ML {*
2.334 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.335 +*}
2.336 +
2.337 +ML {*
2.338 + "artifically inject assumptions";
2.339 + val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
2.340 + val ctxt = insert_assumptions [str2term "x < sub_asm_out",
2.341 + str2term "a < sub_asm_local"] cres;
2.342 + val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
2.343 +*}
2.344 +
2.345 +ML {*
2.346 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.347 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.348 +*}
2.349 +
2.350 +section {* finish subproblem, return to calling method*}
2.351 +
2.352 +text {* transfer non-local assumptions and result from sub-method to root-method.
2.353 + non-local assumptions are those contaning a variable known in root-method.
2.354 +*}
2.355 +
2.356 +ML {*
2.357 + terms2strs (get_assumptions_ pt p);
2.358 +*}
2.359 +
2.360 +ML {*
2.361 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.362 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.363 +*}
2.364 +
2.365 +section {* finish Lucas interpretation *}
2.366 +
2.367 +text {* assumptions collected during lucas-interpretation for proof of postcondition *}
2.368 +
2.369 +ML {*
2.370 + terms2strs (get_assumptions_ pt p);
2.371 +*}
2.372 +
2.373 +ML {*
2.374 + show_pt pt;
2.375 +*}
2.376 +
2.377 +end
2.378 +\end{verbatim}
2.379 +
2.380 +\bibliography{bib}
2.381 \end{document}