1.1 --- a/src/Doc/isac/msteger/bakk-plan.tex Mon Sep 16 12:27:20 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,141 +0,0 @@
1.4 -\documentclass{article}
1.5 -\usepackage{a4}
1.6 -\usepackage{times}
1.7 -\usepackage{latexsym}
1.8 -
1.9 -\bibliographystyle{alpha}
1.10 -\usepackage{graphicx}
1.11 -
1.12 -\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.13 -\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.14 -\def\Problem{ {\tt Problem }}
1.15 -
1.16 -
1.17 -\title{Userinterfaces f\"ur Computer Theorem Prover\\
1.18 - Machbarkeits-Studie im Isac-Projekt
1.19 -}
1.20 -
1.21 -\author{Marco Steger\\
1.22 -Bachelorarbeit Telematik\\
1.23 -am Institut f\"ur Softwaretechnologie\\
1.24 -TU Graz}
1.25 -
1.26 -\begin{document}
1.27 -\maketitle
1.28 -%\newpage
1.29 -\section{Zur Aufgabenstellung der Bachelorarbeit}\label{intro}
1.30 -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.
1.31 -
1.32 -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.
1.33 -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.
1.34 -
1.35 -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.
1.36 -
1.37 -%\newpage
1.38 -
1.39 -\section{Ist-Zustand zu Projektbeginn}
1.40 -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.
1.41 -
1.42 -Sowohl zu jEdit als auch zu Scala und NetBeans bestehen keine Erfahrungen im ISAC-Projekt.
1.43 -
1.44 -\section{Planung: Soll-Zustand am Projektende}
1.45 -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.
1.46 -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.
1.47 -
1.48 -%\newpage
1.49 -
1.50 -\section{Milestones und Arbeitsprotokolle}
1.51 -\subsection{Inhaltliche Voraussetzungen erarbeitet: am 27.09.2010}
1.52 -\begin{itemize}
1.53 -\item Kenntnis der Grundlagen und Anwendung von CTP: am 03.08.2010
1.54 -\item Charakteristika der Programmsprache Scala: 27.09.2010
1.55 -\item Scala Actors: am 12.08.2010
1.56 -\end{itemize}
1.57 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
1.58 -\hline
1.59 -Datum & T\"atigkeit & Einheiten \\ \hline
1.60 -12.07.2010 & Meeting: erste Besprechung und Erklärungen zu Isabelle, Isac und CTPs & 2 \\ \hline
1.61 -15.07.2010 & Recherche über Isabelle und CTPs & 3 \\ \hline
1.62 -20.07.2010 & Meeting: Besprechen der grundsätzlichen Vorgangsweise und Ziele & 1 \\ \hline
1.63 -23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenhänge mit Isac abklären & 1 \\ \hline
1.64 -30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise über Backs 'structured derivations'; Begriffserklärung & 3 \\ \hline
1.65 -01.08.2010 & Recherche: Buch für Scala & 2 \\ \hline
1.66 -03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
1.67 -05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
1.68 -06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
1.69 -08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
1.70 -09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
1.71 -12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
1.72 -24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
1.73 -25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
1.74 -27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline
1.75 - & Anzahl der Einheiten & 44 \\
1.76 -\hline
1.77 -\end{tabular}
1.78 -
1.79 -
1.80 -\subsection{Technische Voraussetzungen hergestellt: am 02.08.2010}
1.81 -\begin{itemize}
1.82 -\item Isabelle installiert, Filestruktur bekannt: am 02.08.2010
1.83 -\item Scala in NetBeans eingebunden: am 22.07.2010
1.84 -\item Mercurial installiert und einrichten des Repositories: 19.07.2010
1.85 -\end{itemize}
1.86 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
1.87 -\hline
1.88 -Datum & T\"atigkeit & Einheiten \\ \hline
1.89 -19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
1.90 -20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
1.91 -21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
1.92 -22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
1.93 -23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausführen: testen & 5 \\ \hline
1.94 -27.07.2010 & Isabelle-jEdit-Plugin: Änderungen an der Projektstruktur & 7 \\ \hline
1.95 -28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
1.96 -29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
1.97 -30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung über Erfahrungen mit Filestruktur & 4 \\ \hline
1.98 -02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
1.99 - & Anzahl der Einheiten & 60 \\
1.100 -\hline
1.101 -\end{tabular}
1.102 -
1.103 -\subsection{NetBeans-Projekt aufgesetzt }% am ..(*)...}
1.104 -\begin{itemize}
1.105 -\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: am 02.08.2010
1.106 -\item jEdit-Plugin: XML-Files für ISAC vorbereitet: am 22.07.2010
1.107 -\item jEdit-Plugin: Source files geschrieben: 19.07.2010
1.108 -\end{itemize}
1.109 -\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
1.110 -\hline
1.111 -Datum & T\"atigkeit & Einheiten \\ \hline
1.112 -10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
1.113 -11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
1.114 -21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
1.115 -22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten für ISAC & 3 \\ \hline
1.116 -24.08.2010 & Umarbeiten des Isabelle-Plugins für ISAC & 6 \\ \hline
1.117 -26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach Lösungen & 3 \\ \hline
1.118 -28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
1.119 -29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
1.120 -30.08.2010 & Isabelle-jEdit-Plugin endlich vollständig lauffähig gebracht & 4 \\ \hline
1.121 -01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
1.122 -04.09.2010 & Umarbeiten des Isabelle-Plugins für ISAC & 5 \\ \hline
1.123 -20.09.2010 & Einrichten des Laptops für Isabelle-Isac & 4 \\ \hline
1.124 -22.09.2010 & Meeting: Fortschrittsbericht, kurze Einführung für Mitstreiter & 3 \\ \hline
1.125 -
1.126 -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
1.127 -30.09.2010 & QN: Start mit übersetzten der Sourcefiles & 5 \\ \hline
1.128 -02.10.2010 & QN: Übersetzten der Sourcefiles & 6 \\ \hline
1.129 -04.10.2010 & QN: Übersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
1.130 -05.10.2010 & QN: QN vollständig in Scala übersetzt, testen & 2 \\ \hline \hline
1.131 - & Anzahl der Einheiten & 71 \\
1.132 -\hline
1.133 -\end{tabular}
1.134 -
1.135 -\subsection{Experimentelle Parser implementiert}% am ..(*)...}
1.136 -\subsection{Pr\"asentation der Arbeit im IST-Seminar }% am ..(*)...}
1.137 -%\newpage
1.138 -
1.139 -\section{Zusammenfassung und R\"uckblick}
1.140 -
1.141 -
1.142 -%\bibliography{CTP-userinterfaces}
1.143 -%\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}
1.144 -\end{document}
1.145 \ No newline at end of file