1.1 --- a/doc-src/isac/msteger/bakk-arbeit/thesis-intro.tex Tue Jun 28 17:09:05 2011 +0200
1.2 +++ b/doc-src/isac/msteger/bakk-arbeit/thesis-intro.tex Fri Jul 01 10:45:12 2011 +0200
1.3 @@ -1,7 +1,9 @@
1.4 \chapter{Einf\"{u}hrung}
1.5 -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.6 +Europa ist bei Computer Theorem Provern (CTP) weltweit f\"uhrend, die zwei prominenten Prover sind Coq \cite{coq1999} und Isabelle \cite{Paulson:Isa94}.
1.7 +Im Zuge der Weiterentwicklung der Informatik als Ingenieurs-Disziplin werden auch Anwendungsgebiete zunehmend mathematisiert \cite{db:dom-eng}, was wiederum CTP vermehrt auf den Plan ruft.
1.8 +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.9
1.10 -Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software- Ingenieuren vorzudringen beginnen \cite{wolff10-boogie}, stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen.
1.11 -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.12 +Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software- Ingenieuren vorzudringen beginnen (siehe zum Beispiel \cite{aichernig:uni-iist-02,aichernig:mut-test}),% \cite{wolff10-boogie},
1.13 +stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen. Einer der Vorschl\"age, wie Theorem Prover mit Front-ends zu verbinden w\"are, findet sich in \cite{Aspinall:2007:FIP:1420412.1420429}. Isabelle geht einen anderen Weg, indem es sich aktuellen technischen Herausforderungen stellt \cite{makarius:isa-scala-jedit}: 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.14
1.15 -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' (SD) sollen auf jEdit und Isabelle aufgesetzt werden. Die Bachelorarbeit liefert die Machbarkeits-Studie f\"ur diesen Schritt.
1.16 +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' (SD) \cite{back-grundy-wright-98} sollen auf jEdit und Isabelle aufgesetzt werden. Die Bachelorarbeit liefert die Machbarkeits-Studie f\"ur diesen Schritt.