|
neuper@41964
|
1 |
\documentclass{article}
|
|
neuper@41964
|
2 |
\usepackage{a4}
|
|
neuper@41964
|
3 |
\usepackage{times}
|
|
neuper@41964
|
4 |
\usepackage{latexsym}
|
|
neuper@41964
|
5 |
|
|
neuper@41964
|
6 |
\bibliographystyle{alpha}
|
|
neuper@41964
|
7 |
\usepackage{graphicx}
|
|
neuper@41964
|
8 |
|
|
neuper@41964
|
9 |
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
|
|
neuper@41964
|
10 |
\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
|
|
neuper@41964
|
11 |
\def\Problem{ {\tt Problem }}
|
|
neuper@41964
|
12 |
|
|
neuper@41964
|
13 |
|
|
neuper@41964
|
14 |
\title{Userinterfaces f\"ur Computer Theorem Prover\\
|
|
neuper@41964
|
15 |
Machbarkeits-Studie im Isac-Projekt
|
|
neuper@41964
|
16 |
}
|
|
neuper@41964
|
17 |
|
|
neuper@41964
|
18 |
\author{Marco Steger\\
|
|
neuper@41964
|
19 |
Bachelorarbeit Telematik\\
|
|
neuper@41964
|
20 |
am Institut f\"ur Softwaretechnologie\\
|
|
neuper@41964
|
21 |
TU Graz}
|
|
neuper@41964
|
22 |
|
|
neuper@41964
|
23 |
\begin{document}
|
|
neuper@41964
|
24 |
\maketitle
|
|
neuper@41964
|
25 |
%\newpage
|
|
neuper@41964
|
26 |
\section{Zur Aufgabenstellung der Bachelorarbeit}\label{intro}
|
|
neuper@41964
|
27 |
Computer Theorem Prover (CTP) sind bis dato in H\"anden eines relativ kleinen Kreises von Experten, von denen der Gro{\ss}teil wiederum im akademischen Bereich arbeitet und nur ein kleiner Teil in der Industrie. Diese Experten bevorzugen Keyboard-Shortcuts (vor Men\"us), reine Texte (ohne mathematische Sonderzeichen) und benutzen auch mit gro{\ss}em Aufwand hergestellte CTP-Entwicklungs-Umgebungen nicht, zum Beispiel die CoqIDE.
|
|
neuper@41964
|
28 |
|
|
neuper@41964
|
29 |
Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software-Ingenieuren vorzudringen beginnen, stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen.
|
|
neuper@41964
|
30 |
Isabelle stellt sich dieser Herausforderung motiviert durch eine aktuelle technische Entwicklung: Multicore-Maschinen versprechen erh\"ohten Durchsatz, falls Teile von Beweisen parallel abgearbeitet werden k\"onnen. Isabelles Entwurf sieht vor, die Programmsprache Scala (insbesonders seine Actor-Library) als Bindeglied zwischen der Mathematik-Sprache SML und der g\"angisten Plattform f\"ur GUIs vor, der Java-Virtual-Maschine.
|
|
neuper@41964
|
31 |
|
|
neuper@41964
|
32 |
Die Bachelorarbeit l\"auft im Rahmen des ISAC-Projektes. ISACs experimenteller Mathematik-Assistant baut auf dem SML-Teil von Isabelle auf und es ist geplant, auch sein Frontend in entsprechend geplanten Schritten an die aktuelle Entwicklung von Isabelle anzuschlie{\ss}en. Der erste Schritt geht einen Umweg, um die Technologie kennen zu lernen: Nicht ISACs Rechnungen (mit aufw\"andigen Interaktionen), sondern Backs 'structured derivations' sollen auf jEdit und Isabelle aufgesetzt werden. Die Bachelorarbeit liefert die Machbarkeits-Studie f\"ur diesen Schritt.
|
|
neuper@41964
|
33 |
|
|
neuper@41964
|
34 |
%\newpage
|
|
neuper@41964
|
35 |
|
|
neuper@41964
|
36 |
\section{Ist-Zustand zu Projektbeginn}
|
|
neuper@41964
|
37 |
ISAC wird als Eclipse-Projekt entwickelt, das das JavaSwing-Frontend und auch die SML-Mathematik-Engine (samt einer alten Isabelle-Version) umfasst. Isabelles kommende jEdit/Scala-Technologie ist schwer in Eclipse zu integrieren. Zwei Frontends, das alte JavaSwing und das neue jEdit, st\"oren sich gegenseitig in einer einzigen Entwicklungs-Umgebung.
|
|
neuper@41964
|
38 |
|
|
neuper@41964
|
39 |
Sowohl zu jEdit als auch zu Scala und NetBeans bestehen keine Erfahrungen im ISAC-Projekt.
|
|
neuper@41964
|
40 |
|
|
neuper@41964
|
41 |
\section{Planung: Soll-Zustand am Projektende}
|
|
neuper@41964
|
42 |
ISAC ist in die Isabelle-Entwicklung integriert, die ISAC-Entwicklung l\"auft in einem updatebaren Repository von Isabelle. F\"ur das in Entwicklung befindliche jEdit-Frontend von Isabelle ist ein NetBeans-Projekt aufgesetzt.
|
|
neuper@41964
|
43 |
Wesentliche Vorarbeiten haben die Herausforderungen gekl\"art, die sich aus der Zielsetzung ergeben: Backs 'structured derivations' \"uber das neue jEdit-GUI eingeben und von Isabelle checken lassen.
|
|
neuper@41964
|
44 |
|
|
neuper@41964
|
45 |
%\newpage
|
|
neuper@41964
|
46 |
|
|
neuper@41964
|
47 |
\section{Milestones und Arbeitsprotokolle}
|
|
neuper@41964
|
48 |
\subsection{Inhaltliche Voraussetzungen erarbeitet: am 27.09.2010}
|
|
neuper@41964
|
49 |
\begin{itemize}
|
|
neuper@41964
|
50 |
\item Kenntnis der Grundlagen und Anwendung von CTP: am 03.08.2010
|
|
neuper@41964
|
51 |
\item Charakteristika der Programmsprache Scala: 27.09.2010
|
|
neuper@41964
|
52 |
\item Scala Actors: am 12.08.2010
|
|
neuper@41964
|
53 |
\end{itemize}
|
|
neuper@41964
|
54 |
\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
|
|
neuper@41964
|
55 |
\hline
|
|
neuper@41964
|
56 |
Datum & T\"atigkeit & Einheiten \\ \hline
|
|
neuper@41964
|
57 |
12.07.2010 & Meeting: erste Besprechung und Erklärungen zu Isabelle, Isac und CTPs & 2 \\ \hline
|
|
neuper@41964
|
58 |
15.07.2010 & Recherche über Isabelle und CTPs & 3 \\ \hline
|
|
neuper@41964
|
59 |
20.07.2010 & Meeting: Besprechen der grundsätzlichen Vorgangsweise und Ziele & 1 \\ \hline
|
|
neuper@41964
|
60 |
23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenhänge mit Isac abklären & 1 \\ \hline
|
|
neuper@41964
|
61 |
30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise über Backs 'structured derivations'; Begriffserklärung & 3 \\ \hline
|
|
neuper@41964
|
62 |
01.08.2010 & Recherche: Buch für Scala & 2 \\ \hline
|
|
neuper@41964
|
63 |
03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
|
|
neuper@41964
|
64 |
05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
|
|
neuper@41964
|
65 |
06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
|
|
neuper@41964
|
66 |
08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
|
|
neuper@41964
|
67 |
09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
|
|
neuper@41964
|
68 |
12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
|
|
neuper@41964
|
69 |
24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
|
|
neuper@41964
|
70 |
25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
|
|
neuper@41964
|
71 |
27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline
|
|
neuper@41964
|
72 |
& Anzahl der Einheiten & 44 \\
|
|
neuper@41964
|
73 |
\hline
|
|
neuper@41964
|
74 |
\end{tabular}
|
|
neuper@41964
|
75 |
|
|
neuper@41964
|
76 |
|
|
neuper@41964
|
77 |
\subsection{Technische Voraussetzungen hergestellt: am 02.08.2010}
|
|
neuper@41964
|
78 |
\begin{itemize}
|
|
neuper@41964
|
79 |
\item Isabelle installiert, Filestruktur bekannt: am 02.08.2010
|
|
neuper@41964
|
80 |
\item Scala in NetBeans eingebunden: am 22.07.2010
|
|
neuper@41964
|
81 |
\item Mercurial installiert und einrichten des Repositories: 19.07.2010
|
|
neuper@41964
|
82 |
\end{itemize}
|
|
neuper@41964
|
83 |
\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
|
|
neuper@41964
|
84 |
\hline
|
|
neuper@41964
|
85 |
Datum & T\"atigkeit & Einheiten \\ \hline
|
|
neuper@41964
|
86 |
19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
|
|
neuper@41964
|
87 |
20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
|
|
neuper@41964
|
88 |
21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
|
|
neuper@41964
|
89 |
22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
|
|
neuper@41964
|
90 |
23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausführen: testen & 5 \\ \hline
|
|
neuper@41964
|
91 |
27.07.2010 & Isabelle-jEdit-Plugin: Änderungen an der Projektstruktur & 7 \\ \hline
|
|
neuper@41964
|
92 |
28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
|
|
neuper@41964
|
93 |
29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
|
|
neuper@41964
|
94 |
30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung über Erfahrungen mit Filestruktur & 4 \\ \hline
|
|
neuper@41964
|
95 |
02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
|
|
neuper@41964
|
96 |
& Anzahl der Einheiten & 60 \\
|
|
neuper@41964
|
97 |
\hline
|
|
neuper@41964
|
98 |
\end{tabular}
|
|
neuper@41964
|
99 |
|
|
neuper@41964
|
100 |
\subsection{NetBeans-Projekt aufgesetzt }% am ..(*)...}
|
|
neuper@41964
|
101 |
\begin{itemize}
|
|
neuper@41964
|
102 |
\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: am 02.08.2010
|
|
neuper@41964
|
103 |
\item jEdit-Plugin: XML-Files für ISAC vorbereitet: am 22.07.2010
|
|
neuper@41964
|
104 |
\item jEdit-Plugin: Source files geschrieben: 19.07.2010
|
|
neuper@41964
|
105 |
\end{itemize}
|
|
neuper@41964
|
106 |
\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
|
|
neuper@41964
|
107 |
\hline
|
|
neuper@41964
|
108 |
Datum & T\"atigkeit & Einheiten \\ \hline
|
|
neuper@41964
|
109 |
10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
|
|
neuper@41964
|
110 |
11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
|
|
neuper@41964
|
111 |
21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
|
|
neuper@41964
|
112 |
22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten für ISAC & 3 \\ \hline
|
|
neuper@41964
|
113 |
24.08.2010 & Umarbeiten des Isabelle-Plugins für ISAC & 6 \\ \hline
|
|
neuper@41964
|
114 |
26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach Lösungen & 3 \\ \hline
|
|
neuper@41964
|
115 |
28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
|
|
neuper@41964
|
116 |
29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
|
|
neuper@41964
|
117 |
30.08.2010 & Isabelle-jEdit-Plugin endlich vollständig lauffähig gebracht & 4 \\ \hline
|
|
neuper@41964
|
118 |
01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
|
|
neuper@41964
|
119 |
04.09.2010 & Umarbeiten des Isabelle-Plugins für ISAC & 5 \\ \hline
|
|
neuper@41964
|
120 |
20.09.2010 & Einrichten des Laptops für Isabelle-Isac & 4 \\ \hline
|
|
neuper@41964
|
121 |
22.09.2010 & Meeting: Fortschrittsbericht, kurze Einführung für Mitstreiter & 3 \\ \hline
|
|
neuper@41964
|
122 |
|
|
neuper@41964
|
123 |
29.09.2010 & Neue Vorgehensweise: QuickNotepad-Plugin(QN) wird in Scala übersetzt und für ISAC entsprechend angepasst: Arbeit an den XML-Files & 4 \\ \hline
|
|
neuper@41964
|
124 |
30.09.2010 & QN: Start mit übersetzten der Sourcefiles & 5 \\ \hline
|
|
neuper@41964
|
125 |
02.10.2010 & QN: Übersetzten der Sourcefiles & 6 \\ \hline
|
|
neuper@41964
|
126 |
04.10.2010 & QN: Übersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
|
|
neuper@41964
|
127 |
05.10.2010 & QN: QN vollständig in Scala übersetzt, testen & 2 \\ \hline \hline
|
|
neuper@41964
|
128 |
& Anzahl der Einheiten & 71 \\
|
|
neuper@41964
|
129 |
\hline
|
|
neuper@41964
|
130 |
\end{tabular}
|
|
neuper@41964
|
131 |
|
|
neuper@41964
|
132 |
\subsection{Experimentelle Parser implementiert}% am ..(*)...}
|
|
neuper@41964
|
133 |
\subsection{Pr\"asentation der Arbeit im IST-Seminar }% am ..(*)...}
|
|
neuper@41964
|
134 |
%\newpage
|
|
neuper@41964
|
135 |
|
|
neuper@41964
|
136 |
\section{Zusammenfassung und R\"uckblick}
|
|
neuper@41964
|
137 |
|
|
neuper@41964
|
138 |
|
|
neuper@41964
|
139 |
%\bibliography{CTP-userinterfaces}
|
|
neuper@41964
|
140 |
%\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}
|
|
neuper@41964
|
141 |
\end{document} |