wneuper/isa: doc-isac/msteger/bakk-arbeit/thesis-title.tex@f8845fc8f38d

     1 % --- English Title Page ------------------------------------------------

     2 \begin{titlepage}

     3 \begin{center}

     4 \vspace*{8mm}

     5 {\LARGE Bachelor's Thesis}\\

     7 \vspace{16mm}

     9 {\huge \bf Userinterfaces for Computer Theorem Provers\\

    10 	Feasibility Study in the \isac-Projekt\\}

    12 \vspace{16mm}

    14 {\LARGE Marco Steger\textsuperscript{1}}\\

    16 \vspace{16mm}

    18 {\Large

    19 Institute for Software Technology (IST)\\

    20 Graz University of Technology\\

    21 A-8010 Graz, Austria\\}

    23 \vspace{16mm}

    25 %TODO TU - figure; Line 26, 76

    26 %\begin{figure}[!ht]

    27 %\centerline{\includegraphics[width=4cm,keepaspectratio=true]{fig/tug}}

    28 %\end{figure}

    30 \vspace{16mm}

    32 {\large

    33 \begin{tabular}{ll}

    34 Advisor:    & Ass.Prof. Dipl.-Ing. Dr.techn.\ Bernhard Aichernig\\[0.5ex]

    35 %TODO Aichernig????

    36 Co-Advisor: & Dr.techn.\ Walther Neuper

    37 \end{tabular}}

    39 \vfill

    40 {\large Graz, 30.06.2011}

    41 \vspace{15mm}

    42 \end{center}

    44 \noindent

    45 \underline{\hspace*{3cm}}\\

    46 {\footnotesize

    47 \textsuperscript{1} E-mail: m.steger@student.tugraz.at\\

    48 \copyright ~ Copyright 2011 by the author}

    52 % --- German Title Page -------------------------------------------------

    53 \selectlanguage{austrian}

    55 \newpage

    56 \begin{center}

    57 \vspace*{8mm}

    58 {\LARGE Bachelorarbeit}\\

    60 \vspace{16mm}

    62 {\huge \bf Userinterfaces f\"ur Computer Theorem Prover\\

    63 	Machbarkeits-Studie im \isac-Projekt\\}

    65 \vspace{16mm}

    67 {\LARGE Marco Steger\textsuperscript{1}}\\

    69 \vspace{16mm}

    71 {\Large

    72 Institut f\"ur Softwaretechnologie (IST)\\

    73 Technische Universit\"at Graz\\

    74 A-8010 Graz\\}

    76 \vspace{16mm}

    78 %\begin{figure}[!ht]

    79 %\centerline{\includegraphics[width=4cm,keepaspectratio=true]{fig/tug}}

    80 %\end{figure}

    82 \vspace{16mm}

    84 %TODO Aichernig????

    85 {\large

    86 \begin{tabular}{ll}

    87 Gutachter:	& Ass.Prof. Dipl.-Ing. Dr.techn.\ Bernhard Aichernig\\[0.5ex]

    88 Mitbetreuer:	& Dr.techn.\ Walther Neuper

    89 \end{tabular}}

    91 \vspace{16mm}

    92 {\large Graz, 30.05.2011}

    94 \vfill

    95 Diese Arbeit ist in deutscher Sprache verfasst.

    96 \end{center}

    98 \noindent

    99 \underline{\hspace*{3cm}}\\

   100 {\footnotesize

   101 \textsuperscript{1} E-Mail: m.steger@student.tugraz.at\\

   102 \copyright ~ Copyright 2011, Marco Steger}

   103 \end{titlepage}

   105 \selectlanguage{english}

   108 % --- English Abstract --------------------------------------------------

   109 \pagestyle{plain}

   110 \pagenumbering{roman}

   111 \newpage

   113 \vspace*{25mm}

   115 \begin{changemargin}{15mm}{15mm}

   116 \begin{center}

   117 {\Large\bfseries Abstract}

   118 \end{center}

   119 \vspace*{7mm}

   121 The computer theorem prover Isabelle switches from a user interface for expert users to a user interface which is more powerful and which serves integration of Isabelle into other tools for software engineers.

   123 This bachelor thesis in ``Telematik'' introduces the specific components underlying Isabelle's new user interface, the scala-layer for asyncronous editing of proof documents, the Java-based editor jEdit together with the respective plugin mechanisms; and the thesis documents the current organization of these components in Isabelle and sets up the whole system, Isabelle, Scala and jEdit in the IDE NetBeans copying the configuration of the Isabelle developer team. This setup is explored in the implementation of a test-plugin, and the experiences are documented in detail.

   125 Thus the prerequisites are given for cooperation in the further development of Isabelle's future front-end and respective integration into development tools like test case generators for software engineers.

   127 \vspace{5mm}

   128 \noindent

   129 {\large\bfseries Keywords:}

   130 computer theorem prover, Isabelle, user-interface, jEdit, plugin, Scala, actors, asynconous communication, proof document, structured derivations

   134 % --- German Abstract ---------------------------------------------------

   135 \selectlanguage{austrian}

   136 \newpage

   138 \vspace*{10mm}

   140 \begin{center}

   141 {\Large\bfseries Kurzfassung}

   142 \end{center}

   143 \vspace*{2mm}

   145 Der Theoremprover Isabelle befindet sich im \"Ubergang von einer Oberfl\"ache f\"ur akademische Benutzer zu einem generellen Frontend, das in verschiedenste softwaretechnische Tools eingebunden werden kann.

   147 Die vorliegende Bachelorarbeit in Telematik f\"uhrt in die speziellen, dem Frontend zugrundleliegenden Konzepte und Komponenten  (Scala-Layer f\"ur asynchrone Bearbeitung von Beweisdokumenten, jEdit mit Plugins, Parser) ein, dokumentiert die momentane Organisation dieser Komponenten im Isabelle System und setzt das gesamte System in einer integrierten Entwicklungsungebung auf. Dieses Setup wird in der Implementation eines Test-Plugins erprobt. Die Erfahrungen mit diesem Test werden ausf\"uhrlich dokumentiert.

   149 Hiermit sind die organisatorischen und softwaretechnische Voraussetzungen daf\"ur geschaffen, dass ein Team an der Technischen Universi\"at Graz an der Entwicklung des kommenden Frontends f\"ur den Theoremprover Isabelle und seiner Integration in Entwicklungswerkzeuge teilhaben kann.

   151 \vspace{5mm}

   152 \noindent

   153 {\large\bfseries Schlagworte:}

   154 Computer Theorem Proving, Isabelle, User-Interface, jEdit, Plugin, Scala, Actors, Asyncrone Kommunikation, Beweis-Dokument, Structured Derivations

   156 \selectlanguage{english}

   157 \end{changemargin}

   160 % --- Pledge ------------------------------------------------------------

   161 \newpage

   162 \vspace*{20mm}

   164 \begin{center}

   165 {\Large\bfseries Statutory Declaration}

   166 \end{center}

   167 \vspace{5mm}

   168 \noindent

   169 I declare that I have authored this thesis independently, that I have not used other than the declared

   170 sources/resources, and that I have explicitly marked all material which has been quoted either

   171 literally or by content from the used sources.

   173 \vspace{2cm}

   175 \noindent

   176 \begin{tabular}{ccc}

   177 \hspace*{6cm}     & \hspace*{2cm}   & \hspace*{6.7cm}\\

   178 \dotfill          &                 & \dotfill\\

   179 place, date       &                 & (signature)\\

   180 \end{tabular}

   182 \vspace{35mm}

   185 \selectlanguage{austrian}

   187 \begin{center}

   188 {\Large\bfseries Eidesstattliche Erkl\"arung}

   189 \end{center}

   190 \vspace{5mm}

   191 \noindent

   192 Ich erkl\"are an Eides statt, dass ich die vorliegende Arbeit selbstst\"andig verfasst, andere als die

   193 angegebenen Quellen/Hilfsmittel nicht benutzt, und die den benutzten Quellen w\"ortlich und inhaltlich

   194 entnommenen Stellen als solche kenntlich gemacht habe.

   196 \vspace{2cm}

   198 \noindent

   199 \begin{tabular}{ccc}

   200 \hspace*{6cm}     & \hspace*{2cm}   & \hspace*{6.7cm}\\

   201 \dotfill          &                 & \dotfill\\

   202 Ort, Datum        &                 & (Unterschrift)\\

   203 \end{tabular}

   205 \selectlanguage{english}

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 17 Sep 2013 09:50:52 +0200
changeset 52107	f8845fc8f38d
parent 52056	src/Doc/isac/msteger/bakk-arbeit/thesis-title.tex@f5d9bceb4dc0
permissions	-rw-r--r--