|
1 \documentclass[a4paper,12pt]{article} |
|
2 |
|
3 \usepackage[ngerman]{babel} |
|
4 \usepackage[utf8]{inputenc} |
|
5 |
|
6 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
7 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
8 |
|
9 \begin{document} |
|
10 |
|
11 \title{\Large {\bf Verbindung von 'Computation' und 'Deduction' im \isac{}-System}\\~\\ |
|
12 Projektpraktikum am Institut für Computersprachen, TU Wien} |
|
13 \author{Mathias Lehnfeld\\ |
|
14 {\tt mathias.lehnfeld@gmx.at}} |
|
15 \maketitle |
|
16 |
|
17 \clearpage |
|
18 |
|
19 |
|
20 \section{Zur Aufgabenstellung} |
|
21 Das \sisac{}-Projekt entwickelt einen {\it math assistant} aufbauend auf den |
|
22 {\it theorem prover} Isabelle. Der Kern des \sisac{}-Systems ist ein |
|
23 {\it Lucas-Interpreter}, der automatisch Benutzerführung für schrittweises |
|
24 Problemlösen erzeugt: Der nächste Schritt wird von einem Programm |
|
25 berechnet ({\it computation}); {\it deduction} wird gefordert, wenn der Benutzer |
|
26 eine Formel eingibt (die Ableitbarkeit der Formel aus dem {\it context} ist |
|
27 zu beweisen).\\ |
|
28 \\ |
|
29 Die Aufgabenstellung im Rahmen des Projektpraktikums besteht darin, das |
|
30 in Isabelle verfügbare Konzept {\it context} in den Lucas-Interpreter |
|
31 einzubauen. Dies schließt grundlegende Design-Überlegungen ein, verlangt |
|
32 tiefes Eindringen in den umfangreichen Code von zwei Softwareprodukten, |
|
33 {\it Isabelle} und \sisac{} und bedeutet daher Zusammenarbeit mit den jeweiligen |
|
34 Entwicklerteams.\\ |
|
35 \\ |
|
36 Ein erfolgreicher Einbau der Isabelle-{\it context}s in den |
|
37 Lucas-Interpreter wird \sisac{}s Fähigkeit, Benutzereingaben zu |
|
38 interpretieren, wesentlich erweitern: {\it context}s stellen Isabelles |
|
39 automatischen Beweisern die notwendigen Daten bereit. |
|
40 |
|
41 \clearpage |
|
42 |
|
43 \section{Planung des Projektinhaltes} |
|
44 \subsection{Ist-Zustand vor dem Projekt} |
|
45 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. |
|
46 |
|
47 \subsection{Geplanter Soll-Zustand nach dem Projekt} |
|
48 \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. |
|
49 |
|
50 \clearpage |
|
51 |
|
52 \section{Dokumentation der Meilensteine} |
|
53 |
|
54 \subsection{Voraussetzungen zum Arbeitsbeginn schaffen} |
|
55 \begin{tabular}[t]{lll} |
|
56 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ |
|
57 10.02.2011 & 2:00 & Besprechung der Problemstellung \\ |
|
58 11.02.2011 & 1:30 & {\it context}s studieren, Isabelle/Mercurial Installation \\ |
|
59 18.02.2011 & 0:15 & meld/tortoisehg installieren \\ |
|
60 20.02.2011 & 1:00 & Projektbeschreibung, jedit Probleme \\ |
|
61 25.02.2011 & 1:00 & Ausarbeitung Meilensteine \\ |
|
62 26.02.2011 & 1:00 & Ausarbeitung Ist-/Soll-Zustand, {\it context}s studieren\\ |
|
63 28.02.2011 & 1:15 & Einführungsbeispiel {\it context}s \\ |
|
64 28.02.2011 & 1:15 & Projektplan erstellen, formatieren \\ |
|
65 01.03.2011 & 1:00 & Projektplan überarbeiten, Stundenlisten \\ |
|
66 \end{tabular} |
|
67 |
|
68 \subsection{\isac{} auf die letzte Isabelle-Release updaten} |
|
69 Die Arbeit mit den Isabelle {\it context}s wird Anfragen in isabelle-dev@ |
|
70 erfordern. isabelle-dev@ beantwortet Fragen i.A. nur für die aktuelle |
|
71 Release. Überraschenderweise wurde vor zwei Wochen eine neue Release |
|
72 veröffentlicht. Daher muss auf diese vor Arbeitsbeginn upgedatet werden.\\ |
|
73 \\ |
|
74 \begin{tabular}[t]{lll} |
|
75 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ |
|
76 18.02.2011 & 2:45 & Anpassungen an Isabelle2011 \\ |
|
77 20.02.2011 & 2:45 & Update auf Isabelle2011, Fehlersuche \\ |
|
78 21.02.2011 & 6:30 & ... \\ |
|
79 25.02.2011 & 5:30 & ... \\ |
|
80 26.02.2011 & 4:30 & ... \\ |
|
81 03.03.2011 & 5:00 & ... \\ |
|
82 04.03.2011 & 6:00 & Tests reparieren \\ |
|
83 \end{tabular} |
|
84 |
|
85 \subsection{Parsen aus {\it context}s} |
|
86 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.\\ |
|
87 \\ |
|
88 \begin{tabular}[t]{lll} |
|
89 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ |
|
90 02.03.2011 & 1:30 & vorbereitendes Übungsbeispiel \\ |
|
91 03.03.2011 & 1:00 & ... \\ |
|
92 04.03.2011 & 5:00 & Funktion {\tt parseNEW} schreiben \\ |
|
93 05.03.2011 & 3:00 & Funktion {\tt vars} anpassen, {\tt declare\_constraints} neu \\ |
|
94 07.03.2011 & 8:45 & {\tt parseNEW}, Spezifikationen studieren \\ |
|
95 08.03.2011 & 6:00 & {\it context} in zentrale Datenstrukturen einbauen \\ |
|
96 09.03.2011 & 2:00 & Fehlersuche {\it context}-Integration \\ |
|
97 \end{tabular} |
|
98 |
|
99 \subsection{Spezifikationsphase mit {\it context}s} |
|
100 \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.\\ |
|
101 \\ |
|
102 \begin{tabular}[t]{lll} |
|
103 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ |
|
104 10.03.2011 & 2:30 & {\it context} in {\tt prep\_ori} und {\tt appl\_add} einbauen\\ |
|
105 11.03.2011 & 5:45 & {\tt appl\_add} überarbeiten \\ |
|
106 12.03.2011 & 5:15 & Fehlersuche \\ |
|
107 14.03.2011 & 2:00 & ... \\ |
|
108 16.03.2011 & 2:30 & ... \\ |
|
109 17.03.2011 & 1:45 & ... \\ |
|
110 18.03.2011 & 4:45 & ..., Optimierung \\ |
|
111 19.03.2011 & 5:30 & ... \\ |
|
112 21.03.2011 & 3:00 & Abschluss Spezifikationsphase \\ |
|
113 \end{tabular} |
|
114 |
|
115 \subsection{Lösungsphase mit {\it context}s} |
|
116 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.\\ |
|
117 \\ |
|
118 \begin{tabular}[t]{lll} |
|
119 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ |
|
120 22.03.2011 & 4:30 & {\it context} in Funktion {\tt solve} einbauen\\ |
|
121 23.03.2011 & 4:45 & Tests reparieren \\ |
|
122 24.03.2011 & 3:30 & ... \\ |
|
123 25.03.2011 & 2:00 & ... \\ |
|
124 03.04.2011 & 4:00 & ... \\ |
|
125 05.04.2011 & 8:00 & Optimierung \\ |
|
126 06.04.2011 & 7:15 & Lösung Exponentenoperator \\ |
|
127 07.03.2011 & 7:00 & ... \\ |
|
128 12.04.2011 & 3:30 & Projektbericht \\ |
|
129 \end{tabular} |
|
130 |
|
131 \section{Bericht zum Projektverlauf} |
|
132 |
|
133 \subsection{Voraussetzungen zum Arbeitsbeginn schaffen} |
|
134 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. |
|
135 |
|
136 \subsection{\isac{} auf die letzte Isabelle-Release updaten} |
|
137 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. |
|
138 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. |
|
139 |
|
140 \subsection{Parsen aus {\it context}s} |
|
141 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. |
|
142 |
|
143 \subsection{Spezifikationsphase mit {\it context}s} |
|
144 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. |
|
145 Insgesamt verlief diese Phase trotz der langwierigen Fehlersuche entsprechend dem Zeitplan. |
|
146 |
|
147 \subsection{Lösungsphase mit {\it context}s} |
|
148 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. |
|
149 |
|
150 |
|
151 \section{Abschließende Bemerkungen} |
|
152 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.\\ |
|
153 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.\\ |
|
154 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. |
|
155 |
|
156 \end{document} |