diff --git a/.gitignore b/.gitignore index 4cb5c97..9592cd5 100644 --- a/.gitignore +++ b/.gitignore @@ -3,5 +3,6 @@ !/.gitignore !/thesis.tex +!/thesis_old.tex !/thesis.pdf !/tuda_logo.pdf diff --git a/thesis.pdf b/thesis.pdf index 2c17838..0c477e7 100644 Binary files a/thesis.pdf and b/thesis.pdf differ diff --git a/thesis.tex b/thesis.tex index 549ac94..862c171 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1,581 +1,476 @@ +%% This is file `DEMO-TUDaThesis.tex' version 3.16 (2021/06/08), +%% it is part of +%% TUDa-CI -- Corporate Design for TU Darmstadt +%% ---------------------------------------------------------------------------- +%% +%% Copyright (C) 2018--2021 by Marei Peischl +%% +%% ============================================================================ +%% This work may be distributed and/or modified under the +%% conditions of the LaTeX Project Public License, either version 1.3c +%% of this license or (at your option) any later version. +%% The latest version of this license is in +%% http://www.latex-project.org/lppl.txt +%% and version 1.3c or later is part of all distributions of LaTeX +%% version 2008/05/04 or later. +%% +%% This work has the LPPL maintenance status `maintained'. +%% +%% The Current Maintainers of this work are +%% Marei Peischl +%% Markus Lazanowski +%% +%% The development respository can be found at +%% https://github.com/tudace/tuda_latex_templates +%% Please use the issue tracker for feedback! +%% +%% If you need a compiled version of this document, have a look at +%% http://mirror.ctan.org/macros/latex/contrib/tuda-ci/doc +%% or at the documentation directory of this package (if installed) +%% /doc/latex/tuda-ci +%% ============================================================================ +%% +% !TeX program = lualatex +%% + +%% This is file `DEMO-TUDaThesis.tex' version 3.16 (2021/06/08), +%% it is part of +%% TUDa-CI -- Corporate Design for TU Darmstadt +%% ---------------------------------------------------------------------------- +%% +%% Copyright (C) 2018--2021 by Marei Peischl +%% +%% ============================================================================ +%% This work may be distributed and/or modified under the +%% conditions of the LaTeX Project Public License, either version 1.3c +%% of this license or (at your option) any later version. +%% The latest version of this license is in +%% http://www.latex-project.org/lppl.txt +%% and version 1.3c or later is part of all distributions of LaTeX +%% version 2008/05/04 or later. +%% +%% This work has the LPPL maintenance status `maintained'. +%% +%% The Current Maintainers of this work are +%% Marei Peischl +%% Markus Lazanowski +%% +%% The development respository can be found at +%% https://github.com/tudace/tuda_latex_templates +%% Please use the issue tracker for feedback! +%% +%% If you need a compiled version of this document, have a look at +%% http://mirror.ctan.org/macros/latex/contrib/tuda-ci/doc +%% or at the documentation directory of this package (if installed) +%% /doc/latex/tuda-ci +%% ============================================================================ +%% +% !TeX program = lualatex +%% + \documentclass[ -article, -accentcolor=9c, -10pt, -colorback=false, -marginpar=false, -pdfa=false % we disable pdf/a mode to achieve easier compilation compatibility + ngerman, + ruledheaders=section,%Ebene bis zu der die Überschriften mit Linien abgetrennt werden, vgl. DEMO-TUDaPub + class=report,% Basisdokumentenklasse. Wählt die Korrespondierende KOMA-Script Klasse + thesis={type=bachelor},% Dokumententyp Thesis, für Dissertationen siehe die Demo-Datei DEMO-TUDaPhd + accentcolor=9c,% Auswahl der Akzentfarbe + custommargins=true,% Ränder werden mithilfe von typearea automatisch berechnet + marginpar=false,% Kopfzeile und Fußzeile erstrecken sich nicht über die Randnotizspalte + %BCOR=5mm,%Bindekorrektur, falls notwendig + parskip=half-,%Absatzkennzeichnung durch Abstand vgl. KOMA-Script + fontsize=11pt,%Basisschriftgröße laut Corporate Design ist mit 9pt häufig zu klein +% logofile=example-image, %Falls die Logo Dateien nicht vorliegen ]{tudapub} -%% you need to install the TUD corporate design LaTex styles -%% https://www.intern.tu-darmstadt.de/arbeitsmittel/corporate_design_vorlagen/index.en.jsp -\usepackage[utf8]{inputenc} +% Der folgende Block ist nur bei pdfTeX auf Versionen vor April 2018 notwendig +\usepackage{iftex} +\ifPDFTeX + \usepackage[utf8]{inputenc}%kompatibilität mit TeX Versionen vor April 2018 +\fi -\usepackage[charter]{mathdesign} -\usepackage{amsmath,amsthm} %% general convenience commands/environments for mathematical typesetting +%%%%%%%%%%%%%%%%%%% +%Sprachanpassung & Verbesserte Trennregeln +%%%%%%%%%%%%%%%%%%% +\usepackage[english, main=ngerman]{babel} +\usepackage[autostyle]{csquotes}% Anführungszeichen vereinfacht -\usepackage{bussproofs} %% useful for setting logic calculi proofs +% Falls mit pdflatex kompiliert wird, wird microtype automatisch geladen, in diesem Fall muss diese Zeile entfernt werden, und falls weiter Optionen hinzugefügt werden sollen, muss dies über +% \PassOptionsToPackage{Optionen}{microtype} +% vor \documentclass hinzugefügt werden. +\usepackage{microtype} -\usepackage{booktabs} %% nicer tables +%%%%%%%%%%%%%%%%%%% +%Literaturverzeichnis +%%%%%%%%%%%%%%%%%%% +\usepackage{biblatex} % Literaturverzeichnis +\bibliography{thesis} -\usepackage{hyperref} %% clickable links -\usepackage[english]{babel} %% if you write in german use \usepackage[ngerman]{babel} -\usepackage[babel]{csquotes} +%%%%%%%%%%%%%%%%%%% +%Paketvorschläge Tabellen +%%%%%%%%%%%%%%%%%%% +%\usepackage{array} % Basispaket für Tabellenkonfiguration, wird von den folgenden automatisch geladen +\usepackage{tabularx} % Tabellen, die sich automatisch der Breite anpassen +%\usepackage{longtable} % Mehrseitige Tabellen +%\usepackage{xltabular} % Mehrseitige Tabellen mit anpassarer Breite +\usepackage{booktabs} % Verbesserte Möglichkeiten für Tabellenlayout über horizontale Linien -\usepackage[makeroom]{cancel} +%%%%%%%%%%%%%%%%%%% +%Paketvorschläge Mathematik +%%%%%%%%%%%%%%%%%%% +%\usepackage{mathtools} % erweiterte Fassung von amsmath +%\usepackage{amssymb} % erweiterter Zeichensatz +%\usepackage{siunitx} % Einheiten -\usepackage{color} -\usepackage{tcolorbox} +%Formatierungen für Beispiele in diesem Dokument. Im Allgemeinen nicht notwendig! +\let\file\texttt +\let\code\texttt +\let\tbs\textbackslash +\let\pck\textsf +\let\cls\textsf -\usepackage{epstopdf} - -\usepackage{caption} -\usepackage{fix-cm} -\usepackage{fontspec} - -\usepackage{float} -\usepackage[newfloat]{minted} - -% \usepackage{microtype} -% \usepackage{hyphenat} -% \usepackage{seqsplit} - -% \usepackage{titling} -% \usepackage{titlesec} -% \usepackage{titletoc} - -\usepackage{hyperref} - -\hypersetup{ - colorlinks=true, - linkcolor=magenta, - urlcolor=blue, - pageanchor=false -} - -\makeatletter -\renewcommand{\minted@inputpyg}{% - \expandafter\let\expandafter\minted@PYGstyle% - \csname PYG\minted@get@opt{style}{default}\endcsname - \VerbatimPygments{\PYG}{\minted@PYGstyle}% - \ifthenelse{\boolean{minted@isinline}}% - {\ifthenelse{\equal{\minted@get@opt{breaklines}{false}}{true}}% - {\let\FV@BeginVBox\relax - \let\FV@EndVBox\relax - \def\FV@BProcessLine##1{% - \FancyVerbFormatLine{% - \FV@BreakByTokenAnywhereHook - \FancyVerbFormatText{\FancyVerbBreakStart##1\FancyVerbBreakStop}}}% - \minted@inputpyg@inline}% - {\minted@inputpyg@inline}}% - {\minted@inputpyg@block}% -} -\makeatother - -\setminted{breaklines=true,breakanywhere=true,breakbytoken=false,breakbytokenanywhere=false,tabsize=4,frame=single,framesep=.5em,samepage=false} -\setmintedinline{breaklines=true,breakanywhere=true,breakbytoken=false,breakbytokenanywhere=false} - -\newenvironment{mintedlisting}{% - \begin{listing}[H]% - \captionsetup{% - format=plain,% - width=.75\textwidth,% - type=listing,% - justification=centering,% - singlelinecheck=off,% - position=bottom,% - skip=0pt,% - name=Code-Listing% - }% -}{% - \end{listing}% -} - -\newcommand{\hreffn}[2]{\href{#1}{#2}\footnote{#1}} - -\newcommand{\tbs}{\textbackslash} - -\title{Bachelor Thesis} -\subtitle{% -B. Sc. Informatik Thesis\\ -FG Software Engineering (Prof.\ Dr.\ Reiner H\"ahnle)\\ -Supervisor: Lukas Grätz -} -\author{David Holland} - -\addTitleBoxLogo{se-logo.pdf} +\usepackage{pifont}% Zapf-Dingbats Symbole +\newcommand*{\FeatureTrue}{\ding{52}} +\newcommand*{\FeatureFalse}{\ding{56}} \begin{document} +\Metadata{ + title=Integration von Hilbert's Epsilon-Operator in KeY, + author=David Holland +} + +\title{Integration von Hilbert's $\varepsilon$-Operator in KeY} +\subtitle{% +FG Software Engineering (Prof. Dr. Reiner Hähnle)\\ +Supervisor: Lukas Grätz +} +\author[D. Holland]{David Holland}%optionales Argument ist die Signatur, +\birthplace{Wiesbaden-Dotzheim}%Geburtsort, bei Dissertationen zwingend notwendig +\reviewer{Prof. Dr. Reiner Hähnle \and Lukas Grätz}%Gutachter + +%Diese Felder erden untereinander auf der Titelseite platziert. +%\department ist eine notwendige Angabe, siehe auch dem Abschnitt `Abweichung von den Vorgaben für die Titelseite' +\department{ce} % Das Kürzel wird automatisch ersetzt und als Studienfach gewählt, siehe Liste der Kürzel im Dokument. +\institute{Institut} +\group{Arbeitsgruppe} + +\submissiondate{\today} +\examdate{\today} + +% Hinweis zur Lizenz: +% TUDa-CI verwendet momentan die Lizenz CC BY-NC-ND 2.0 DE als Voreinstellung. +% Die TU Darmstadt hat jedoch die Empfehlung von dieser auf die liberalere +% CC BY 4.0 geändert. Diese erlaubt eine Verwendung bearbeiteter Versionen und +% die kommerzielle Nutzung. +% TUDa-CI wird im nächsten größeren Release ebenfalls diese Anpassung vornehmen. +% Aus diesem Grund wird empfohlen die Lizenz manuell auszuwählen. +% \tuprints{urn=1234,printid=12345,doi=10.25534/tuprints-1234,license=cc-by-4.0} +% To see furhter information on the license option in English, remove the license= key and pay attention to the warning & help message. + +% \dedication{Für alle, die \TeX{} nutzen.} + \maketitle -\section{Motivation} - -To explain the necessity of the following elaborations, as well as to ground the motivation, I will use the following java class, which implements a demonstration of a high score table. -The functionality of this class is that \texttt{scores} consists of the highest values added to the high score table by \texttt{addScore}. - -\begin{minted}{java} -public class HighSoreTable { - int[] scores = new int[10]; - /** - * adds a new score to the high score list - * @param newScore newScore to add - * @return 0 when not added (since below 10 best) - * 2 if new high score - * 1 if otherwise - */ - public int addScore(int newScore) { - int min = 0; - boolean maxScore = true; - for (int i=0; i < 10; i++) { - if (scores[i] < scores[min]) { - min = 1; - } - if (newScore <= scores[i]) { - maxScore = false; - } - } - if (newScore <= scores[min]) { - return 0; - } - scores[min] = newScore; - return maxScore ?2 :1; - } -} -\end{minted} - -If I now want to be able to verify its correctness using KeY, I have to annotate the class with JML first. -I won't bother annotating this class to completion, which would include also specifying invariants for the \texttt{for} loop, as well as specifying invariants for the array modifications. - -\begin{minted}{java} -public class HighSoreTable { - int[] scores = new int[10]; - /** - * adds a new score to the high score list - * @param newScore newScore to add - * @return 0 when not added (since below 10 best) - * 2 if new high score - * 1 if otherwise - */ - /*@ requires newScore >= 0; - @ ensures (\forall int i; 0<=i && i<10; - @ newScore <= \old(scores[i]) - @ ) - @ ==> (\result == 0); - @ ensures (\exists int i; 0<=i && i<10; - @ newScore > \old(scores[i]) - @ ) - @ && (\exists int i; 0<=i && i<10; - @ newScore <= \old(scores[i]) - @ ) - @ ==> (\result == 1); - @ ensures (\forall int i; 0<=i && i<10; - @ newScore > \old(scores[i]) - @ ) - @ ==> (\result == 2); - @*/ - public int addScore(int newScore) { - // [...] - } -} -\end{minted} - -As one can see, while being functional, as well as delivering the intended result, this example definitely is very verbose and not very practical, as the lack of readability, as well as the big redundancy could introduce bugs, unintended behaviour, etc. during modification or similar. - -To mitigate this issue, there are two main ways, one of which I will discuss in-depth as the topic of my thesis and the other one of which I will possibly still have to utilize to achieve the intended result. - -\subsection{Macros} - -I will start to shortly explain the solution first, which I won't discuss as a main topic within my thesis, namely the usage of \emph{macros}. -This method improves code reusage and in consequence also readability. - -\begin{minted}{java} -public class HighSoreTable { - int[] scores = new int[10]; - /** - * adds a new score to the high score list - * @param newScore newScore to add - * @return 0 when not added (since below 10 best) - * 2 if new high score - * 1 if otherwise - */ - //@ requires newScore >= 0; - /*@ def lowerThanMin(score) = - @ (\forall int i; 0<=i && i<10; - @ score <= \old(scores[i]) - @ ); - @*/ - //@ ensures lowerThanMin(newScore) ==> (\result == 0); - // [...] - public int addScore(int newScore) { - // [...] - } -} -\end{minted} - -Note hoewever that the notion of macros is currently neither implemented in JML, nor KeY, so this solution would be subject to an implementation from my side. -For implementing this, I could use the concept of a preprocessor, which simply expands all occurrences of defined macros with their definition. - -So for example - -\begin{minted}{java} -/*@ def lowerThanMin(score) = - @ (\forall int i; 0<=i && i<10; - @ score <= \old(scores[i]) - @ ); - @*/ -//@ ensures lowerThanMin(newScore) ==> (\result == 0); -\end{minted} - -would get expanded to - -\begin{minted}{java} -//@ ensures (\forall int i; 0<=i && i<10; newScore <= \old(scores[i])); ==> (\result == 0); -\end{minted} - -However there are multiple issues I see with this approach. - -First off, it would make debugging the code with KeY magnitudes harder, as the developer would never get to see the expanded code (s.a.), but in contrast the parser, etc. would only see the expanded code. -This means that if there is a type mismatch for example which would throw a compiler error, the error would complain about a code point which the developer never gets to see. -One would need to manually search \& replace the whole code, in other words expanding the macros manually, to see what KeY complains about, which would make this feature completely useless. - -In the case of a type mismatch between macro parameter usage and parameter input by the caller, it could theoretically be mitigated by introducing typed macro parameters, which in turn makes the macro more of a named lambda, in which case however it wouldn't be feasible anymore to just use a "dumb" macro expansion. - -\begin{minted}{java} -/*@ def lowerThanMin(int score) = - @ (\forall int i; 0<=i && i<10; - @ score <= \old(scores[i]) - @ ); - @*/ -//@ ensures lowerThanMin(newScore) ==> (\result == 0); -\end{minted} - -or alternatively, to serve the lambda notion more - -\begin{minted}{java} -//@ lowerThanMin = (int score) -> (\forall int i; 0<=i && i<10; score <= \old(scores[i])); -//@ ensures lowerThanMin(newScore) ==> (\result == 0); -\end{minted} - -Another problem not solved by this approach, especially not with using a simplistic macro expansion, would be the problem of infinite recursion, which is not really sensible in this example, but should be kept in mind anyways. - -\begin{minted}{java} -/*@ def lowerThanMin(int score) = - @ (\forall int i; 0<=i && i<10; - @ score <= \old(scores[i]) - @ && lowerThanMin(score-1) - @ ); - @*/ -//@ ensures lowerThanMin(newScore) ==> (\result == 0); -\end{minted} - -\subsection{$\varepsilon$-operator} - -As mentioned above, there is another way to mitigate the problem of unreadable code. -One of the problems of the original JML is that it can prove to be more complex to understand. -One example of such a case is that even though $\neg \exists x \in M \neg (x < a)$ expresses the exact same thing as $\forall x \in M (x < a)$, the first term is magnitudes harder to understand immediately, which makes the second term more expressive. -Of course the first term has the "advantage" of not needing a $\forall$, but sacrifices intuitive understanding for that. - -An analogy can be made for our discussed example. -Instead of defining a \emph{method} on \emph{how} it can be determined if a \emph{given score} is lower than the minimal score of the high score table, we could define the \emph{property} of a minimal score, which we could then compare our \emph{given score} to. -This property of a minimal score can then be reused and clearly states what it denotes, therefore improving readability and code reusage. - -\begin{minted}{java} -/*@ def minScore = - @ (\some int score; - @ (\exists int i; 0<=i && i<10; score == scores[i]) - @ && (\forall int i; 0<=i && i<10; score <= scores[i]) - @ ); - @*/ -//@ ensures newScore <= \old(minScore) ==> (\result ==0); -\end{minted} - -This notion of a \emph{property} definition, for which there exists \texttt{some} value that fulfills it, is called \emph{Hilbert's $\varepsilon$-term}. -Compared to the analogy given previously, the second example utilizes a new \texttt{\tbs{}some} which improves the understanding of what the \texttt{minScore} \emph{is} instead of just determining \emph{a} lowest score. -In the following paragraphs I'll investigate this method further. - -This example introduces the keyword \texttt{\tbs{}some}. -Other possible keywords with a similar notion would be \texttt{\tbs{}all}, as well as \texttt{\tbs{}one}. -The naming of those keywords makes it pretty obvious what intended their behaviour is. - -\texttt{\tbs{}one} selects \emph{the one} value fulfilling the specified conditional property. -This means there can only be one value doing so and respectively that the handling of multiple values fulfilling the condition is the same as if there were none. -This is a so called \emph{definite description} and denoted by $\iota$, where $\iota_{x}A(x)$ denotes \emph{the} object $x$ with a property $A$. - -\texttt{\tbs{}some} selects \emph{some} value non-deterministically, which fulfills a specified conditional property. -At this point, it isn't of any interest \emph{which} value exactly is selected, it is only of importance that it does fulfill the property definition. -This is a so called \emph{indefinite description} and denoted by $\varepsilon$, where $\varepsilon_{x}A(x)$ denotes \emph{some} object $x$ with a property $A$. - -\texttt{\tbs{}all} in turn selects \emph{all} values fulfilling the specified conditional property. -This means there can be \emph{one} or \emph{multiple} values doing so. - -There already are theories used to solve the aforementioned scenarios, especially in the case of \texttt{\tbs{}some}. -The notion described by this keyword is called \emph{Hilbert's $\varepsilon$-operator} and there are methods to check theories for consistency using this operator. - -I can however see some challenges with the implementation of this concept. -First of epsilon terms are nondeterministic. -This means that \emph{if} multiple values fulfill the conditional property, the selection of one of those values is non-deterministic. -This makes it very hard to implement in a real-world application computational system, as our classical computational components can't really make real non-deterministic decisions. -The nature of KeY might come to the rescue though, as the implementation would need to construct a \emph{proof} using this epsilon-operator, rather than computing some real values. -Checking a theory for consistency is possible in the epsilon-calulus and is called the \emph{epsilon substitution method}. - -The other challenge is in the nature of the epsilon calculus. -The epsilon calculus can express first-order-logic (FOL), but not the other way around. -This means that the epsilon calculus \emph{extends} the FOL calulus. -This is validated by looking at the epsilon substitution method, where it is mandatory that among other preocedures, the theory to be checked is embedded in an epsilon calculus and all quatified theorems are replaced by epsilon operations. - -The easiest thing, in terms of complexity of the challenges, etc., to implement from scratch in a normal software development setting, would probably be the \texttt{one} keyword, as that is the notion of the \emph{definite description}. -In this case I neither have to deal with the epsilon calculus, nor the non-deterministic nature. -% It's easiest to understand for the software developer. But implementation is magnitudes. -\emph{However} in terms of constructing proofs (read implementing it for KeY) I would rate the complexity \emph{much} higher compared to \texttt{\tbs{}some}! -Proving that any value out of a defined set is fulfilling a condition is in my understanding way easier than proving that either \texttt{\tbs{}all} or even exactly \texttt{\tbs{}one} does so. - -It is also worth noting that usability extends far beyond the showcased example. -It would be thinkable to use those keywords outside of a reusable and non-redundant code design and just use them "in-line". -This also means that an introduction of a "named property" would still be required to achieve the goals showcased throghout this section. -That's why I mentioned that the need to have some kind of "dumb" macro, which would make it possible to assign a name to this epsilon-term, might still arise. -I have to investigate how I could utilize the already implemented (within KeY) notion of \emph{ghost variables}. - -Luckily an already implemented function of KeY could be used, modified, or at least used as a foundation for the proposed functionality. -The name of the class is \texttt{IfExThenElse} which one can use using the JML operator \texttt{\tbs{}ifEx}. -If we reference the \hreffn{http://i12www.ira.uka.de/~key/download/nightly/api/}{documentation for this class}, we can see some description on how to use it - -\[ - \mathrm{\tbs{}ifEx\ } i; (\phi)\ \mathrm{\tbs{}then\ } (t_1)\ \mathrm{\tbs{}else\ } (t2) -\] - -This conditional operator \texttt{\tbs{}ifEx} will check an integer logic variable $i$, which occurs in bound form within a formula $\phi$ and a term $t_1$, and proceed with term $t_1$ or $t_2$ respective of whether the bound variable can fulfull the formula $\phi$ for \emph{some} value. - -An implementation could therefore be possible using something like this pseudo code snippet: - -\begin{minted}{java} -/*@ def minScore = - @ (\ifEx int score; - @ (\exists int i; 0<=i && i<10; score == scores[i]) - @ && (\forall int i; 0<=i && i<10; score <= scores[i]) - @ \then - @ return score - @ \else - @ return None - @ ); - @*/ -//@ ensures newScore <= \old(minScore) ==> (\result == 0); -\end{minted} - -Note that in this example some value gets "returned". -This is probably not something you would want to achieve in KeY. -We wanted to describe the \emph{property} of a minimal score, not have a concrete value fulfilling this property. -This could also be something some kind of ghosting variable could achieve, but I would need to investigate this further. - -For the time being, one could inline this whole concept and possibly have a working example, though this would not necessarily improve either readability or code reusage, but definitely increase versatility and expressiveness. - -\begin{minted}{java} -/*@ ensures - @ (\ifEx int minScore; - @ (\exists int i; 0<=i && i<10; minScore == scores[i]) - @ && (\forall int i; 0<=i && i<10; minScore <= scores[i]) - @ \then - @ newScore <= minScore ==> (\result == 0) - @ \else - @ \result != 0 - @ ); - @*/ -\end{minted} - -Note however that I noticed the \texttt{\tbs{}else} branch is not really doing what it should be. -The else part doesn't handle the case of the \texttt{newScore} being higher than the minScore! -Instead it is handling the case when \emph{no} \texttt{minScore}, with the property of being an element in the \texttt{scores} array, as well as being the smallest element in this array, exists! -So in this case this would mean that our high score table is empty. -So this branch should either throw some kind of error, or rather make sure the ensures doesn't evaluate to true in that case, if this behaviour is not allowed, or if this is allowed, handle this case differently. -In case it isn't allowed to have an empty high score table, the example should be like follows - -\begin{minted}{java} -/*@ ensures - @ (\ifEx int minScore; - @ (\exists int i; 0<=i && i<10; minScore == scores[i]) - @ && - @ (\forall int i; 0<=i && i<10; minScore <= scores[i]) - @ \then - @ newScore <= minScore ==> (\result == 0) - @ \else - @ false - @ ); - @*/ -\end{minted} - -The main difficulty of this approach is the handling of the bound variable, the way of returning the notion of the fulfilling value to the caller, as in the notion of a value matching the property description, as well as handling the case of no value fulfilling the formula. - -In my opinion one could either use some sort of \texttt{null} value, or some sort of an \texttt{option} type. -With the \texttt{null} value, the "caller" would be in need of some kind of checking if such a \texttt{null} value has been returned. -With the \texttt{option} type could lift this burden from the user and put it on the compiler/runtime/etc. -The option type is a commonly used type in the programming language rust. -In this context the generic option type, initialized with a concrete type, either holds an instance of the specified type, or it holds the \emph{nothing} value. -Therefore one calls a mehtod on the option type either returning the instance of the specified type, or it raises and exception. -It would be interesting to investigate if this kind of behaviour would benefit this cause. - -\subsection{Conclusion} - -I think it might well be necessary to employ both proposed solutions together. -As I mentioned, defining and implementing some kind of epsilon-terms is useful in itsefl as it would greatly increase KeY, JavaDL, etc. in terms of versatility and expressiveness. -It would however not improve the original points of critique, namely redundancy and low readability. -To do that one would have to be able to \emph{name} a property, so it can be reused at multiple code points and upon finding an error, or edge case within a property definition, being able to change it in one centralized place and being sure that no other code point is in need of modification. -This would therefore raise the need of some kind of naming, which could be either solved by some kind of ghosting variable, or some simplistic macro handling. - -\newpage - -\section{Work Packages} - -I think the work lying ahead of me is contained withing the following work subjects. - -\begin{enumerate} - \item Research how \texttt{\tbs{}ifEx} is implemented within JavaDL and/or KeY, in order to be able to implement something smilar myself. - This should teach me all I need in terms of which source files are linked together or are standing in relation to one another, as well as how the different parts play together to create something that KeY can use for constructing a proof. - Try implementing or extending some placeholder functionality in order to get a feel for it. - - \item Research how I can implement the aforementioned epsilon substitution method. - Possibly research how such a notion is implemented in Java in general, or other programming languages that serve the intent of proof construction or proving code correctness more, like e.g. functional programming languages like Haskell. - - \item Research how ghosting variables could be used to achieve the wanted effect. - If this is not feasible, I would have to think about employing some kind of macros. - - \item Research how other programming languages implement macro handling, as well as to what extent. - This would greatly improve the understanding of whether this task, even if it only serves the purpose of naming the properties, is as easy as employing a preprocessor, or if some more intricate handling is necessary. - - \item Research which parts are implemented within KeY itself and which are implemented within JavaDL. - This will greatly help my understanding of the underlying working mechanisms of KeY, how they work together to construct proofs, etc. - - \item Possibly implement a minimal working example using \texttt{\tbs{}ifEx} to see in which cases it is lacking, or if it is already sufficient compared to the expected behaviour of a (blackbox implementation) \texttt{\tbs{}some}. - If not, I would have to manually implement the aforementioned keywords. - Therefore the goal of this task would be to determine if it would be feasible to embed the \texttt{\tbs{}ifEx} into a \texttt{\tbs{}some} keywoard or if a groud-up approach is necessary. - - \item Determine (using this minimal working example) what the true goal to be achieved through this thesis is, to have a concrete expectation horizon. - - \item Implement \texttt{some} with a minimal scope of functionality, i.e. a minimal working example. - According to how easy/difficult this task is, it is determined if implementation of \texttt{one} and/or \texttt{all} is workable within the given 6 months timeframe. - - \item Implement some kind of naming mechanism for the property definition. - - \item Construct multiple usage examples to demo and test the new functionality. - - \item Write extensive tests and also theoretically ground the approach and implementation to ensure issue-free usage. - - \item Document the implementation as well as the whole process to maintain reproducability. - - \item Write the thesis itself. - -\end{enumerate} - -\section{Schedule} - -I would estimate the amount of work needed to take (almost) all of these points to completion to be workable within the given timeframe of the thesis, namely 6 months. -I will expect to write the documentation as well as snippets of sections of the final thesis during the whole duration. -I will also expect to have the finalization of the thesis as well as the presentation take 6 weeks or more by themselves. -Apart from that I will mainly focus on finishing the rough research part as fast as possible, in order for me to determine wheter a complete implementation from scratch is needed or not. -Note however that this is subject to great fluctuation as well as change, as I can't really estimate the amount of work, further research, implementation and documentation that needs to be done. -Also note that for some tasks a non-sequential completion can be possible. - -\section{Challenges} - -When trying to implement this new token \texttt{\tbs{}some}, I encountered many hurdles. -Especially since some things, in particular \texttt{\tbs{}ifEx}, have some special quirks, limitation and/or boundaries in KeY at the time of writing my thesis, it took quite some time to get behind of all the underlying behaviour and inner workings of the code base, in order to ensure a clean implementation of the wanted token. - -\subsubsection{\texttt{\tbs{}some} as a quantifier} -First of all the question arose, in what form this token should be incorporated into the KeY codebase. -I decided to implement it as an extension of a collection of quantifiers withing KeY. - -Up to this point, the quantifiers available through JML were -\begin{itemize} - \item \texttt{\tbs{}forall} - \item \texttt{\tbs{}exists} - \item \texttt{\tbs{}min} - \item \texttt{\tbs{}max} - \item \texttt{\tbs{}sum} - \item \texttt{\tbs{}num\_of} -\end{itemize} - -By extending this collection of tokens with a new token \texttt{\tbs{}some}, we can utilize the generalized methods for the so called \emph{spec-quantified expressions}, that follow the syntax \texttt{LPAREN quantifier (boundvarmodifiers)? quantifiedvardecls SEMI (expression SEMI)? expression RPAREN}. -This means we can write a some statement the following way: - -\begin{minted}{java} -/*@ ensures (\some T quantifiedVariable; property; defaultValue) > someValue */ -\end{minted} - -In spoken speech form this wouuld mean that \emph{some} \texttt{quantifiedVariable} of type \texttt{T} defined by its \texttt{property} is greater than \texttt{someValue}. -If there is no \texttt{quantifiedVariable} of type \texttt{T} with the specified \texttt{property}, the \texttt{defaultValue} is returned instead and checked against it being greater than \texttt{someValue}. - -Furthermore the following holds true - -\begin{minted}{text} -(\some T var; (property); (defaultValue)) - -<==> - -(\ifEx T var; (property); \then (var) \else (defaultValue)) -\end{minted} - -Because of the somewhat unsual use of the second term for the \texttt{defaultValue}, it imposes some problems on the implementation -% TODO: elaborate - -\texttt{\tbs{}one} could also be implemented like this - -\begin{minted}{text} -(\one T var; (property); (defaultValue)) - -<==> - -(\ifEx - T var; - ( - property - && - (\forall T var2; - (property); - var==var2 - ) - ) - \then - (var) - \else - (defaultValue) -) - -<==> - -(\some T var; - ( - property - && - (\forall T var2; - (property); - var==var2 - ) - ); - defaultValue -) -\end{minted} - - -% \begin{verbatim} -% y = a.m() -% [...] -% await y? -% [...] -% \end{minted} -% -% \begin{figure} -% -% \includegraphics[page=124,width=\textwidth,trim=35 80 25 110,clip]{Presentation_final_slides.pdf} -% -% \caption{Example global MHP graph snippet showcasing direct MHP \cite{MHPA_ABC}} -% \label{fig:mhp-graph-big-direct} -% \end{figure} - -%\bibliographystyle{plain} -%% add the bibliography you want to use in the file below -%% you do not need to create bibtex entries by your self, -%% a good source is https://dblp.uni-trier.de (use the format without crossreferences) -%\bibliography{proposal} +\affidavit[digital]% oder \affidavit falls keine rein digitale Abgabe vorgesehen ist. + +\tableofcontents + +\chapter{Thesis} + +\section{Abstract} +\section{Introduction} +\section{Related Work} +\section{Contribution} +\section{Foundations} +\section{Approach} +\section{Evaluation} +\section{Conclusion \& Future Work} + +\chapter{Über diese Datei} +Die Datei \file{DEMO-TUDaThesis.tex} ist ein Template für Abschlussarbeiten im Stil des Corporate Designs der TU Darmstadt. +Sie ist Teil des TUDa-CI-Bundles wurde vom in Teilen tuddesign-Paket von C.~v.~Loewenich und J.~Werner inspiriert. + +Sie verwendet die Dokumentenklasse \file{tudapub.cls}, allerdings mit erweiterten Einstellungen. In diesem Dokument werden überwiegend die speziell auf Abschlussarbeiten ausgelegten Möglichkeiten beschrieben. Weitere Konfigurationsmöglichkeiten finden sich in der Datei \file{DEMO-TUDaPub.pdf} \cite{tudapub}. + +Es ist voreingestellt, dass eine PDF/A-Datei erzeugt wird. Die beste Kompatibilität hierfür bietet Lua\LaTeX. Bei anderen Compilern kann dies entsprechend der Angaben in DEMO-TUDaPub zu Problemen führen. In diesem Fall sollte entweder der Compiler gewechselt oder \code{pdfa=false} aktiviert werden. + +Für weitere Hinweise kann ein Blick in die zur Dokumentenklasse gehörigen Dokumentation (DEMO-TUDaPub.pdf) hilfreich sein. Sie wird zusammen mit den Quelldateien verteilt. + +\minisec{Unterschiede der Demodateien DEMO-TUDaThesis und DEMO-TUDaPhD} +Zwar basieren alle drei DEMO-Dateien auf der Klasse \code{tudapub}, allerdings sind die Basiseinstelungen dem Dokumententyp angepasst. +Für Erläuterungen zu den TUDaPub spezifischen Optionen, sei auf die Datei DEMO-TUDaPub verwiesen. +Da die Basisklasse für beide identisch ist, kann jede Option abgeändert werden. Die Folgende Liste zeigt lediglich die gezeigten Features bei Standardeinstellungen. + +\noindent\begin{tabularx}{\linewidth}{@{}p{.25\linewidth}*3{>{\centering\arraybackslash}X}@{}} + \toprule + Option&DEMO-TUDaThesis&DEMO-TUDaPhD&DEMO-TUDapub\\ + \midrule + twoside&\FeatureFalse&\FeatureTrue&\FeatureFalse\\\midrule + parskip&\FeatureTrue&\FeatureFalse&\FeatureTrue\\\midrule + Kolophon&\FeatureFalse&\FeatureTrue&\FeatureFalse\\\midrule + Widmung&\FeatureFalse&\FeatureTrue&\FeatureFalse\\\midrule + Schriftgröße&11pt&11pt&9pt\\\midrule + ruledheaders§ion&chapter&all\\\midrule + Basisklasse&scrreprt&scrbook&scrartcl\\\midrule + thesis&\ttfamily type=bachelor&\ttfamily type=dr, dr=rernat + &\FeatureFalse\\\midrule + marginpar&\FeatureFalse&\FeatureFalse&\FeatureTrue\\\midrule + Affidavit\newline\rlap{(Selbstständigkeitserklärung)}&\FeatureTrue&\FeatureTrue&\FeatureFalse\\\midrule + abstract&\FeatureFalse&\FeatureTrue&\FeatureTrue\\\midrule + custommargins&\FeatureTrue&\FeatureTrue&\FeatureFalse\\ + \bottomrule +\end{tabularx} + + +\chapter{Verwendung} +Die Klasse kann wie für Dokumentenklassen üblich eingebunden werden +\begin{verbatim} +\documentclass[thesis]{tudapub} +\end{verbatim} +Die Option \code{thesis} wechselt hierbei in den Modus, der spezielle Features für Abschlussarbeiten freischaltet, die in diesem Dokument beschrieben werden. + +Darüber hinaus lässt sich die Klasse verwenden wie die Standard-KOMA-Script-Klasse, auf der sie basiert. +Voreingestellt ist hierbei \code{scrreprt}. + +Allgemein bietet \KOMAScript{} viele Möglichkeiten zu Anpassungen. Wie in der tudapub-Demo-Datei beschrieben, können hier jedoch nicht alle erläutert werden, ein Blick in die offizielle Dokumentation ist daher häufig hilfreich \cite{scrguide}. + +\section{Sprachanpassung} +Der Modus für Abschlussarbeiten setzt einige sprachabhängige Bezeichnungen. +Teilweise ist Deutsch für diese Elemente als Hauptsprache vorgeschrieben (z.\,B. die Selbstständigkeitserklärung). Für die korrekte Verarbeitung wird daher ein Paket zur Sprachanpassung benötigt. +TUDa-CI verwendet hierfür das babel-Paket. + +Dies wird jedoch nicht automatisch geladen, da hierfür die Konfiguration der Sprachen bekannt sein müsste. Die Demo-Dateien für Abschlussarbeiten (\file{DEMO-TUDaThesis.tex}/""\file{DEMO-TUDaPhD.tex}) laden hierfür die Konfiguration: +\begin{verbatim} + \usepackage[english, main=ngerman]{babel} +\end{verbatim} +Diese ist für ein Dokument mit Deutsch als Hauptsprache und Englischen Elementen. +Die Hauptsprache wird als Wert der Option \verb+main=+ übergeben. +Das Laden von \verb+ngerman+ wird in den Fällen, in denen es von TUDa-CI benötigt wird, automatisch ausgelöst. +Für eine bessere Übersichtlichkeit ist es dennoch hilfreich es dort aufzuführen. + +Falls die Hauptsprache nicht Deutsch ist, wäre daher die folgende Konfiguration sinnvoll: +\begin{verbatim} + \usepackage[ngerman, main=]{babel} +\end{verbatim} + +\section{Übergabe der Titeldaten} + +Die Daten werden analog zur klassichen Titeleierzeugung mit \verb+\maketitle+ übergeben. Allerdings wurden die Felder um ein paar speziellere Daten erweitert. Sofern nicht anders angegeben, verfügen alle Makros über ein notwendiges Argument für die Datenübergabe, z.\,B. +\begin{verbatim} +\title{\LaTeX{} im Corporate Design der TU Darmstadt} +\end{verbatim} +Es ist zu beachten, dass für die Erzeugung der Titelseite nach Übergabe aller Daten \verb+\maketitle+ aufgerufen werden muss. + +\begin{description}\setkomafont{descriptionlabel}{\ttfamily\textbackslash} + \item[title] Titel, wird in sehr großer Schrift im obersten Block der Titelseite platziert. Die Schriftgröße ist aufgrund der Häufigkeit für lange Titel kleiner gewählt als für andere Publikationen. + \item[subtitle] Untertitel. Dieses Feld kann alternativ für eine Übersetzung genutzt werden. + \item[author] Der Autor/dir Autoren. Mehere Autoren werden durch \verb+\and+ getrennt. + \item[studentID] Matrikelnummer. Nach den Vorgaben des Templates ist diese Angabe immer optional. + \item[birthplace] Geburtsort. Angabe ist bei Dissertationen notwendig. + \item[reviewer] Gutachter. Mehrere Gutachter werden, wie Autoren durch \verb+\and+ getrennt. Die Nummerierung läuft von links nach rechts. + \minisec{Änderung des Bezeichners} + Die Änderung des Bezeichners ist über ein optionales Argument möglich: + \begin{verbatim} + \reviewer[Ersatzbezeichner]{Name1 \and Name2} + \end{verbatim} + Um die numerische Benennung abzuändern ist es zusätzlich möglich statt dem Ersatzbezeichner eine Kommaliste zu übergeben: + \begin{verbatim} + \reviewer*[Bezeichner1, Bezeichner2]{Name1 \and Name2} + \end{verbatim} + In diesem Fall entfällt die Nummerierung vor dem Bezeichner. Soll z.\,B. den Formulierungen der Promotionsordnung entsprochen werden, gilt: + \begin{verbatim} + \reviewer[Erstreferent\_in,Koreferent\_in]{Name1 \and Name2} + \end{verbatim} + Für die Erstellung Fachbereichsspezifischer Templates existiert hierfür auch ein Makro, dass ohne den Aufruf von \verb+\reviewer+ Änderungen zulässt. + \begin{verbatim} + \setupReviewName{Ersatzwort für „Gutachten“} + \end{verbatim} + Setzt die ersten beiden Bezeichner. Alternativ ist es auch möglich Positionen einzeln zu benennen \verb+\setupReviewName[1]{Erstferent}+, eine Übergabe als Komma-Liste ist als \verb+\setupReviewName*{Bezeicher1,Bezeicher2}+ möglich. + \item[institution] Einrichtung. Dieser Eintrag, wie auch die beiden folgenden, werden unterhalb des Logos auf der Titelseite platziert. + \item[department] Fach-/Studienbereich, allerdings ist die oben genannte Option zu bevorzugen. Die Verarbeitung des Arguments erfolgt jedoch analog. + + Dieses Makro verfügt jedoch zusätzlich über die Möglichkeit abweichende Einträge gegenüber den Vorgaben anzugeben. Insbesondere wenn eine gesonderte Formulierung gegenüber der voreingestellten \enquote{im Fachbereich} und ihren Varianten notwendig ist. Hierfür liefert \code{\textbackslash{}department} ein optionales Argument: + + \begin{verbatim} + \department[Ersatztext]{Kürzel/Bezeichnung} + \end{verbatim} + Zusätzlich gibt es ab Version 2.01 auch die Möglichkeit den gesamten Text \enquote{im Fachbereich }, sowie die Angabe in der Infobox auf der Titelseite zu ersetzen. Dies geschieht über die gesternte Variante: + \begin{verbatim} + \department*[Text für die Box]{Text zwischen Typ und Autor} + \end{verbatim} + \item[group] Arbeitsgruppe. + \item[submissiondate] Datum der Einreichung + \item[examdate] Datum der Disputation + \item[date] Beliebiges Datum. Wird über \verb|datename| bezeichnet. + \item[publishers] Wird hier für die Ortsangabe verwendet und ist mit \enquote{Darmstadt}, bzw. \enquote{Darmstadt -- D17} (bei Dissertationen) vorbelegt. + \item[tuprints] \label{page:tuprints}Übergabe der Daten, sofern das dokument über tuprints Veröffentlicht werden soll. + \begin{verbatim} + \tuprints{ + urn=1234, + printid=12345, + doi=10.25534/tuprints-1234 + } + \end{verbatim} + Falls das Argument kein Gleichheitszeichen erkennt, wird der Wert als \code{printid} gesetzt und keine URN angegeben. + + Ab Version 2.07 ist es zudem möglich einen eigenen Lizenztext über den Schlüssel \verb|license| zu übergeben. Dieser ersetzt dann die voreingestellte Lizenzangabe. + + Ab Version 3.08 existieren vorgefertigte Werte für die Option \verb|license|, um eine einfachere Anpassung zu ermöglichen. + Dies ist Bestandteil der Vorbereitung zur Anpassung der Standardlizenz, die durch die Universitätsbibliothek angepasst wurde. + Die entsprechende Diskussion findet sich unter \url{https://github.com/tudace/tuda_latex_templates/issues/251} und eine Anpassung der Voreinstellung bei TUDa-CI ist für Version 4.0 vorgesehen. + + Die vorgefertigten Lizenzschlüssel lauten: \verb+cc-by-nc-nd-2.0-de+ (noch aktuelle Voreinstellung), \verb+cc-by-4.0+, \verb+cc-by-sa-4.0+, \verb+cc-by-nc-sa-4.0+, \verb+cc-by-nc-4.0+, \verb+cc-by-nd-4.0+, \verb+cc-by-nc-nd-4.0+. + Unterstützung bei der Wahl einer passenden Creative Commons Lizenz bietet das Projekt über seinen Lizenzfinder unter \url{http://creativecommons.org/choose/}. + Ab Version 3.10 werden alle (Stand: Januar 2021) dort vorgeschlagenen Lizenzen von tuda-ci unterstützt. + + Falls ein davon abweichender Wert gewählt wird, wird dieser direkt an der Stelle des Lizenztextes verwendet. Falls der Text Gleichheitszeichen oder Kommata enthält ist eine Gruppierung notwendig. + \item[titleimage] Hier kann Code übergeben werden, der den farbigen Block im unteren Teil der Titelseite ersetzt. Als Maße können hier die Längen \verb+\layerwidth+ und \verb+\layerheight+ verwendet werden. Sie passen sich dem Verfügbaren Platz an. Für ein Beispiel sei auf die TUDapub-Dokumentation verwiesen. + \item[titleintro] Ab Version 2.03 kann zusätzlich über diesen Hook ein beliebiger Text direkt nach dem Untertitel und vor den automatischen Daten ergänzt werden. + \item[titleaddendum] Wie \code{\tbs{}titleintro} jedoch als letztes Element des Blocks. +\end{description} + +\section{Weitere Macros} +Das Makro \verb+\affidavit+ erzeugt eine Selbstständigkeitserklärung mit Unterschriftenzeile. Hier wird der oben übergebene Name/Signatur eingefügt. +In diesem Dokument findet sich das Affidavit direkt nach der Titelei. + +Ab Version 3.06 verfügt \verb+\affidavit+ zusätzlich über ein optionales Argument, über das der Modus eingestellt werden kann. +Es besteht die Unterscheidung zwischen \verb+digital+ und \verb+print+. Hier wird entsprechend der Vorgabe unter \url{https://www.tu-darmstadt.de/studieren/studierende_tu/studienorganisation_und_tucan/hilfe_und_faq/artikel_details_de_en_37824.de.jsp} der entsprechende Text automatisch ausgewählt. + +\begin{verbatim} +\affidavit[digital] +\end{verbatim} + +Da für Dissertationen bisher keine Option der rein digitalen Abgabe besteht, entfällt dort diese Unterscheidungsmöglichkeit. + +Es besteht zusätzlich die Möglichkeit ein anderssprachiges Affidavit als Ergänzung mit abzudrucken. Um die Struktur und die ggf. notwendige Sprachumschaltung zu erledigen, existiert hierfür ab Version 2.03 eine Umgebung: + +\begin{verbatim} +\begin{affidavit*}[Babel-Sprachoption]{Überschrift} +Text +\end{affidavit*} +\end{verbatim} + +Diese Variante verfügt bewusst über keine Unterschriftenzeile, da diese Version laut Verständnis der Entwickler keine rechtliche Verbindlichkeit besitzt. + +Die Umgebung kann jedoch auch für besondere Formen der Erklärung genutzt werden. In diesem Fall kann eine zusätzliche Signaturzeile über +\begin{verbatim} +\AffidavitSignature[Stadt] +\end{verbatim} +hinzugefügt werden. Die Vorbelegung für Stadt ist hierbei \enquote{Darmstadt}. + +\section{Layout-Optionen mit Verstoß gegen das Corporate Design} + +Die Zeilenlängen sind laut Corporate Design aus typografischer Sicht zu lang. +Daher existiert die Klassenoption \code{custommargins}, die für dieses Dokument aktiviert wurde (Wert \code{true}). Sie verfügt über die Werte \code{true}, \code{false} und \code{geometry} mit folgender Bedeutung: + +\begin{description} +\item[custommargins=false] Standardeinstellung von \cls{tudapub}. Die Ränder entsprechen den Vorgaben des Corporate Design Guidelines. Die Einstellung wird durch \pck{geometry} durchgeführt. Eigene Anpassungen werden durch das Ausführen von \code{\textbackslash{}maketitle} überschrieben. +\item[custommargins=true] Die Einstellungen des Corporate Design Guidelines werden nicht aktiviert. \pck{geometry} wird nicht geladen. Dieser Modus entspricht der Standardeinstellung von \KOMAScript{}. Dadurch werden die Ränder nicht fest definiert, sondern auf Basis des \pck{typearea}-Paketes berechnet \cite[vgl.][]{scrguide}. +\item[custommargins=geometry] Diese Variante wurde auf Wunsch zur Verfügung gestellt, allerdings wird darauf hingewiesen, dass manuelle Randeinstellungen oft nicht zu einem harmonischen Satzspiegel führt. +\pck{geometry} wird, wie bei \code{false} geladen und vorkonfiguriert. Es ist allerdings möglich kleinere Anpassung durch die Verwendung des Makros \code{\textbackslash{}geometry} zu setzen. Die Einstellungen, die zu Beginn des Dokuments gelten werden gespeichert und nach der Titelseite wiederhergestellt. + +Hierbei ist zu beachten, dass die Einstellungen als Ausgangspunkt den Voreingestellten Satzspiegel nutzen (je nach Option mit Randnotizspalte oder ohne). Es ist möglich diese Optionen vor den eigenen mit zurückzusetzen: +\begin{verbatim} + \geometry{ + reset, + + } +\end{verbatim} +Die gilt insbesondere für die Optionen \code{includehead}, \code{includefoot} und \code{includemp}. +\end{description} + + +\minisec{Hinweis zu den Kopf-/Fußzeilen} +Wenn die Option \code{marginpar=true} gesetzt bleibt, ragen die Kopf- und Fußzeile über die Marginalspalte hinaus. Aus ästhetischen Gründen wird daher empfohlen in diesem Fall die Kopf- und Fußzeile mit \code{marginpar=false} auf den Textbereich zu beschränken. + +Auch ist das Standard-Layout der Kolumnentitel wenig vorteilhaft, da die Kolumnentitel damit local größer sein können als die eigentliche Überschrift. (\code{headline=automark}) +Deswegen kann über +\begin{verbatim} + \pagestyle{TUDa.headings} +\end{verbatim} +ein einfacherer Seitenstil ausgewählt werden, der die Nutzung mit lebenden Kolumnentitel erheblich vereinfacht. Dieser Stil ist über \pck{scrlayer-scrpage} realisiert und kann entsprechend der \KOMAScript{}-Dokumentation angepasst werden. + +\minisec{Hinweis zur Bindekorrektur} +Bei Verwendung einer Bindekorrektur (\code{BCOR=}) wird diese nicht automatisch auch auf der Titelseite eingefügt. Für diesen Fall wurde mit Version 3.0 zusätzlich die Option \code{BCORtitlepage} hinzugefügt. Falls diese aktiviert wird, nimmt die Titelseite den Wert der Typearea Option \code{BCOR} auf der ersten Seite als Zusatz zum linken Rand hinzu. + + + +\section{Spezielle Optionen für Abschlussarbeiten} +Die Klasse unterstützt alle Optionen der \file{tudapub}-Klasse. Darüber hinaus besteht über Wertzuweisung der Option \code{thesis} die Möglichkeit spezielle Einstellungen zu wählen. +Es ist prinzipiell möglich die Optionen auch direkt als Optionen zur \file{tudapub}-Klasse zu übergeben, allerdings ist dies aufgrund der schlechteren Übersicht nicht zu empfehlen. + +Für dieses Dokument wurden beispielsweise die Optionen als +\begin{verbatim} +thesis={type=drfinal,dr=phil} +\end{verbatim} +übergeben. + +Im folgenden findet sich die Bedeutung der einzelnen Optionen: +\begin{description} +\item[type=] Auswahl des Typus. Dieser wird auf die Titelseite gesetzt und wählt zudem aus welche Daten für die Titelseite zwingend übergeben werden müssen. + Es stehen die folgenden Werte zur Verfügung (die Werte in Klammern sind die notwendigen Titeldaten): + \begin{itemize} + \item \code{sta}: Studienarbeit (title, author, date) + \item \code{diplom}: Diplomarbeit (title, author, submissiondate, reviewer, department) + \item \code{bachelor}: Bachelorarbeit (title, author, submissiondate, department, reviewer) + \item \code{master}: Masterarbeit (title, author, submissiondate, department, reviewer) + \item \code{pp}: Project-Proposal (title, author, date, department) + \item \code{dr}: vorgelegte Dissertation (title, author, submissiondate , birthplace, department, reviewer) + \item \code{drfinal}: genehmigte Dissertation (title, author, submissiondate,examdate, birthplace, department, reviewer) + \end{itemize} + Wird ein Typus angegeben, der nicht erkannt wird, so wird der Text direkt übergeben. Notwendige Titelfelder über den Titel hinaus gibt es in diesem Fall nicht. +\item[dr=] Lädt einen der vordefinierten Texte für die Titelseite. Als Werte stehen bislang \code{rernat}, \code{ing} und \code{phil} zur Verfügung. Zum Beispiel lädt der Wert \code{phil}: + \begin{quote} + Zur Erlangung des Grades eines Doktor der Philosophie (Dr.\,phil.) + \end{quote} + Sofern keiner dieser Werte dem angestrebten Titel entspricht, kann ein Text direkt übergeben werden. + \begin{verbatim} + \drtext{Zur Erlangung des Grades \ldots} + \end{verbatim} +\item[department=] Die Fachbereiche sind fest als Textbausteine in Deutscher sowie Englischer Sprache hinterlegt. Diese Option ermöglicht die Auswahl als Dokumentenklassenoption. Aus Kompatibilitätsgründen kann jedoch auch das Makro \code{department}-Makro hierfür genutzt werden. Zur Verfügung stehen:\par + \begin{tabular}{@{}l@{${}\to{}$}l@{}} + arch & Architektur\\ + bauing& Bau- und Umweltingenieurwissenschaften\\ + bio &Biologie\\ + chem &Chemie\\ + etit &Elektrotechnik und Informationstechnik\\ + gugw &Gesellschafts- und Geschichtswissenschaften\\ + humanw&Humanwissenschaften\\ + inf &Informatik\\ + mb &Maschinenbau\\ + matgeo&Material- und Geowissenschaften\\ + math &Mathematik\\ + phys &Physik\\ + wi &Rechts- und Wirtschaftswissenschaften + \end{tabular} + + Neben den Fachbereichen existieren für Abschlussarbeiten, die keine Dissertationen sind auch Studienbereiche. + Falls das Kürzel nicht als Fachbereich hinterlegt ist, wird automatisch auf die Studienbereiche geprüft. Die Studienbereiche haben die folgenden Kürzel: + + \begin{tabular}{@{}l@{${}\to{}$}l@{}} + ce&Computational Engineering\\ + ese&Energy Science and Engineering\\ + ist&Information Systems Engineering\\ + mech&Mechanik\\ + metro&Mechatronik + \end{tabular} + + Falls etwas anderes als eines dieser Kürzel übergeben wird, wird der Text direkt verwendet und eine entsprechende Warnung ausgegeben. + + Die Auswahl der Fachrichtung erzeugt zusätzlich eine Box auf der Titelseite unterhalb des Logos. Falls diese automatische Erstellung nicht gewünscht ist, kann dies über die Option \code{instbox=false} deaktiviert werden. +\item[ignore-missing-data] Diese Option ist ein Schalter, der es ermöglicht die Fehlermeldung über nicht übergebene Titeldaten auszuschalten. In diesem Fall wird lediglich eine Warnung erzeugt, falls die angegeben Daten nicht mit den Anforderungen übereinstimmen. +\end{description} + +\minisec{Abweichung von den Vorgaben für die Titelseite} +Da es möglich sein kann von dieser Vorgabe abzuweichen, existiert für Sonderfälle die Dokumentenklassenoption \code{instbox=false}. Damit wird die automatische Verarbeitung der Daten für die Boxen auf der der Titelseite unterdrückt. In diesem Fall ist der Autor jedoch selbst für die Einhaltung der Vorschriften verantwortlich. Weitere Information zur Konstruktion der Boxen findet sich in den Verwendungshinweisen der Basisklasse TUDaPub. Zusätzlich sei auf die Möglichkeiten des \code{\textbackslash{}department}-Makros verwiesen, sofern die Abweichung sich auf den Text beschränkt. + +\section{Erhöhter Zeilenabstand -- Hinweise zum setspace-Paket} +Sofern die Vorgaben es erfordern, ist es möglich mit dem setspace-Paket den Durchschuss zu erhöhen. Allerdings beeinflusst dies natürlich sämtliche Zeilenabstände. Ein erhöhter Zeilenabstand sollte daher erst nach der Titelseite aktiviert werden. Allgemein ist es jedoch empfehlenswert auch für Verzeichnisse und sonstige Sonderelemente außerhalb des Fließtextes auf bei normalen Einstellungen zu bleiben. + +Setspace liefert hierfür die Möglichkeit, das Paket ohne Optionen zu laden und später über Makros, wie \code{\tbs{}onehalfspacing} das Umschalten zu verzögern. Alternativ kann auch durch die Umgebungen, wie \code{singlespace} lokal wieder zum Normalzustand gewechselt werden, sofern dies erforderlich ist. + +\printbibliography \end{document} diff --git a/thesis_old.tex b/thesis_old.tex new file mode 100644 index 0000000..549ac94 --- /dev/null +++ b/thesis_old.tex @@ -0,0 +1,581 @@ +\documentclass[ +article, +accentcolor=9c, +10pt, +colorback=false, +marginpar=false, +pdfa=false % we disable pdf/a mode to achieve easier compilation compatibility +]{tudapub} + +%% you need to install the TUD corporate design LaTex styles +%% https://www.intern.tu-darmstadt.de/arbeitsmittel/corporate_design_vorlagen/index.en.jsp + +\usepackage[utf8]{inputenc} + +\usepackage[charter]{mathdesign} +\usepackage{amsmath,amsthm} %% general convenience commands/environments for mathematical typesetting + +\usepackage{bussproofs} %% useful for setting logic calculi proofs + +\usepackage{booktabs} %% nicer tables + +\usepackage{hyperref} %% clickable links + +\usepackage[english]{babel} %% if you write in german use \usepackage[ngerman]{babel} +\usepackage[babel]{csquotes} + +\usepackage[makeroom]{cancel} + +\usepackage{color} +\usepackage{tcolorbox} + +\usepackage{epstopdf} + +\usepackage{caption} +\usepackage{fix-cm} +\usepackage{fontspec} + +\usepackage{float} +\usepackage[newfloat]{minted} + +% \usepackage{microtype} +% \usepackage{hyphenat} +% \usepackage{seqsplit} + +% \usepackage{titling} +% \usepackage{titlesec} +% \usepackage{titletoc} + +\usepackage{hyperref} + +\hypersetup{ + colorlinks=true, + linkcolor=magenta, + urlcolor=blue, + pageanchor=false +} + +\makeatletter +\renewcommand{\minted@inputpyg}{% + \expandafter\let\expandafter\minted@PYGstyle% + \csname PYG\minted@get@opt{style}{default}\endcsname + \VerbatimPygments{\PYG}{\minted@PYGstyle}% + \ifthenelse{\boolean{minted@isinline}}% + {\ifthenelse{\equal{\minted@get@opt{breaklines}{false}}{true}}% + {\let\FV@BeginVBox\relax + \let\FV@EndVBox\relax + \def\FV@BProcessLine##1{% + \FancyVerbFormatLine{% + \FV@BreakByTokenAnywhereHook + \FancyVerbFormatText{\FancyVerbBreakStart##1\FancyVerbBreakStop}}}% + \minted@inputpyg@inline}% + {\minted@inputpyg@inline}}% + {\minted@inputpyg@block}% +} +\makeatother + +\setminted{breaklines=true,breakanywhere=true,breakbytoken=false,breakbytokenanywhere=false,tabsize=4,frame=single,framesep=.5em,samepage=false} +\setmintedinline{breaklines=true,breakanywhere=true,breakbytoken=false,breakbytokenanywhere=false} + +\newenvironment{mintedlisting}{% + \begin{listing}[H]% + \captionsetup{% + format=plain,% + width=.75\textwidth,% + type=listing,% + justification=centering,% + singlelinecheck=off,% + position=bottom,% + skip=0pt,% + name=Code-Listing% + }% +}{% + \end{listing}% +} + +\newcommand{\hreffn}[2]{\href{#1}{#2}\footnote{#1}} + +\newcommand{\tbs}{\textbackslash} + +\title{Bachelor Thesis} +\subtitle{% +B. Sc. Informatik Thesis\\ +FG Software Engineering (Prof.\ Dr.\ Reiner H\"ahnle)\\ +Supervisor: Lukas Grätz +} +\author{David Holland} + +\addTitleBoxLogo{se-logo.pdf} + +\begin{document} + +\maketitle + +\section{Motivation} + +To explain the necessity of the following elaborations, as well as to ground the motivation, I will use the following java class, which implements a demonstration of a high score table. +The functionality of this class is that \texttt{scores} consists of the highest values added to the high score table by \texttt{addScore}. + +\begin{minted}{java} +public class HighSoreTable { + int[] scores = new int[10]; + /** + * adds a new score to the high score list + * @param newScore newScore to add + * @return 0 when not added (since below 10 best) + * 2 if new high score + * 1 if otherwise + */ + public int addScore(int newScore) { + int min = 0; + boolean maxScore = true; + for (int i=0; i < 10; i++) { + if (scores[i] < scores[min]) { + min = 1; + } + if (newScore <= scores[i]) { + maxScore = false; + } + } + if (newScore <= scores[min]) { + return 0; + } + scores[min] = newScore; + return maxScore ?2 :1; + } +} +\end{minted} + +If I now want to be able to verify its correctness using KeY, I have to annotate the class with JML first. +I won't bother annotating this class to completion, which would include also specifying invariants for the \texttt{for} loop, as well as specifying invariants for the array modifications. + +\begin{minted}{java} +public class HighSoreTable { + int[] scores = new int[10]; + /** + * adds a new score to the high score list + * @param newScore newScore to add + * @return 0 when not added (since below 10 best) + * 2 if new high score + * 1 if otherwise + */ + /*@ requires newScore >= 0; + @ ensures (\forall int i; 0<=i && i<10; + @ newScore <= \old(scores[i]) + @ ) + @ ==> (\result == 0); + @ ensures (\exists int i; 0<=i && i<10; + @ newScore > \old(scores[i]) + @ ) + @ && (\exists int i; 0<=i && i<10; + @ newScore <= \old(scores[i]) + @ ) + @ ==> (\result == 1); + @ ensures (\forall int i; 0<=i && i<10; + @ newScore > \old(scores[i]) + @ ) + @ ==> (\result == 2); + @*/ + public int addScore(int newScore) { + // [...] + } +} +\end{minted} + +As one can see, while being functional, as well as delivering the intended result, this example definitely is very verbose and not very practical, as the lack of readability, as well as the big redundancy could introduce bugs, unintended behaviour, etc. during modification or similar. + +To mitigate this issue, there are two main ways, one of which I will discuss in-depth as the topic of my thesis and the other one of which I will possibly still have to utilize to achieve the intended result. + +\subsection{Macros} + +I will start to shortly explain the solution first, which I won't discuss as a main topic within my thesis, namely the usage of \emph{macros}. +This method improves code reusage and in consequence also readability. + +\begin{minted}{java} +public class HighSoreTable { + int[] scores = new int[10]; + /** + * adds a new score to the high score list + * @param newScore newScore to add + * @return 0 when not added (since below 10 best) + * 2 if new high score + * 1 if otherwise + */ + //@ requires newScore >= 0; + /*@ def lowerThanMin(score) = + @ (\forall int i; 0<=i && i<10; + @ score <= \old(scores[i]) + @ ); + @*/ + //@ ensures lowerThanMin(newScore) ==> (\result == 0); + // [...] + public int addScore(int newScore) { + // [...] + } +} +\end{minted} + +Note hoewever that the notion of macros is currently neither implemented in JML, nor KeY, so this solution would be subject to an implementation from my side. +For implementing this, I could use the concept of a preprocessor, which simply expands all occurrences of defined macros with their definition. + +So for example + +\begin{minted}{java} +/*@ def lowerThanMin(score) = + @ (\forall int i; 0<=i && i<10; + @ score <= \old(scores[i]) + @ ); + @*/ +//@ ensures lowerThanMin(newScore) ==> (\result == 0); +\end{minted} + +would get expanded to + +\begin{minted}{java} +//@ ensures (\forall int i; 0<=i && i<10; newScore <= \old(scores[i])); ==> (\result == 0); +\end{minted} + +However there are multiple issues I see with this approach. + +First off, it would make debugging the code with KeY magnitudes harder, as the developer would never get to see the expanded code (s.a.), but in contrast the parser, etc. would only see the expanded code. +This means that if there is a type mismatch for example which would throw a compiler error, the error would complain about a code point which the developer never gets to see. +One would need to manually search \& replace the whole code, in other words expanding the macros manually, to see what KeY complains about, which would make this feature completely useless. + +In the case of a type mismatch between macro parameter usage and parameter input by the caller, it could theoretically be mitigated by introducing typed macro parameters, which in turn makes the macro more of a named lambda, in which case however it wouldn't be feasible anymore to just use a "dumb" macro expansion. + +\begin{minted}{java} +/*@ def lowerThanMin(int score) = + @ (\forall int i; 0<=i && i<10; + @ score <= \old(scores[i]) + @ ); + @*/ +//@ ensures lowerThanMin(newScore) ==> (\result == 0); +\end{minted} + +or alternatively, to serve the lambda notion more + +\begin{minted}{java} +//@ lowerThanMin = (int score) -> (\forall int i; 0<=i && i<10; score <= \old(scores[i])); +//@ ensures lowerThanMin(newScore) ==> (\result == 0); +\end{minted} + +Another problem not solved by this approach, especially not with using a simplistic macro expansion, would be the problem of infinite recursion, which is not really sensible in this example, but should be kept in mind anyways. + +\begin{minted}{java} +/*@ def lowerThanMin(int score) = + @ (\forall int i; 0<=i && i<10; + @ score <= \old(scores[i]) + @ && lowerThanMin(score-1) + @ ); + @*/ +//@ ensures lowerThanMin(newScore) ==> (\result == 0); +\end{minted} + +\subsection{$\varepsilon$-operator} + +As mentioned above, there is another way to mitigate the problem of unreadable code. +One of the problems of the original JML is that it can prove to be more complex to understand. +One example of such a case is that even though $\neg \exists x \in M \neg (x < a)$ expresses the exact same thing as $\forall x \in M (x < a)$, the first term is magnitudes harder to understand immediately, which makes the second term more expressive. +Of course the first term has the "advantage" of not needing a $\forall$, but sacrifices intuitive understanding for that. + +An analogy can be made for our discussed example. +Instead of defining a \emph{method} on \emph{how} it can be determined if a \emph{given score} is lower than the minimal score of the high score table, we could define the \emph{property} of a minimal score, which we could then compare our \emph{given score} to. +This property of a minimal score can then be reused and clearly states what it denotes, therefore improving readability and code reusage. + +\begin{minted}{java} +/*@ def minScore = + @ (\some int score; + @ (\exists int i; 0<=i && i<10; score == scores[i]) + @ && (\forall int i; 0<=i && i<10; score <= scores[i]) + @ ); + @*/ +//@ ensures newScore <= \old(minScore) ==> (\result ==0); +\end{minted} + +This notion of a \emph{property} definition, for which there exists \texttt{some} value that fulfills it, is called \emph{Hilbert's $\varepsilon$-term}. +Compared to the analogy given previously, the second example utilizes a new \texttt{\tbs{}some} which improves the understanding of what the \texttt{minScore} \emph{is} instead of just determining \emph{a} lowest score. +In the following paragraphs I'll investigate this method further. + +This example introduces the keyword \texttt{\tbs{}some}. +Other possible keywords with a similar notion would be \texttt{\tbs{}all}, as well as \texttt{\tbs{}one}. +The naming of those keywords makes it pretty obvious what intended their behaviour is. + +\texttt{\tbs{}one} selects \emph{the one} value fulfilling the specified conditional property. +This means there can only be one value doing so and respectively that the handling of multiple values fulfilling the condition is the same as if there were none. +This is a so called \emph{definite description} and denoted by $\iota$, where $\iota_{x}A(x)$ denotes \emph{the} object $x$ with a property $A$. + +\texttt{\tbs{}some} selects \emph{some} value non-deterministically, which fulfills a specified conditional property. +At this point, it isn't of any interest \emph{which} value exactly is selected, it is only of importance that it does fulfill the property definition. +This is a so called \emph{indefinite description} and denoted by $\varepsilon$, where $\varepsilon_{x}A(x)$ denotes \emph{some} object $x$ with a property $A$. + +\texttt{\tbs{}all} in turn selects \emph{all} values fulfilling the specified conditional property. +This means there can be \emph{one} or \emph{multiple} values doing so. + +There already are theories used to solve the aforementioned scenarios, especially in the case of \texttt{\tbs{}some}. +The notion described by this keyword is called \emph{Hilbert's $\varepsilon$-operator} and there are methods to check theories for consistency using this operator. + +I can however see some challenges with the implementation of this concept. +First of epsilon terms are nondeterministic. +This means that \emph{if} multiple values fulfill the conditional property, the selection of one of those values is non-deterministic. +This makes it very hard to implement in a real-world application computational system, as our classical computational components can't really make real non-deterministic decisions. +The nature of KeY might come to the rescue though, as the implementation would need to construct a \emph{proof} using this epsilon-operator, rather than computing some real values. +Checking a theory for consistency is possible in the epsilon-calulus and is called the \emph{epsilon substitution method}. + +The other challenge is in the nature of the epsilon calculus. +The epsilon calculus can express first-order-logic (FOL), but not the other way around. +This means that the epsilon calculus \emph{extends} the FOL calulus. +This is validated by looking at the epsilon substitution method, where it is mandatory that among other preocedures, the theory to be checked is embedded in an epsilon calculus and all quatified theorems are replaced by epsilon operations. + +The easiest thing, in terms of complexity of the challenges, etc., to implement from scratch in a normal software development setting, would probably be the \texttt{one} keyword, as that is the notion of the \emph{definite description}. +In this case I neither have to deal with the epsilon calculus, nor the non-deterministic nature. +% It's easiest to understand for the software developer. But implementation is magnitudes. +\emph{However} in terms of constructing proofs (read implementing it for KeY) I would rate the complexity \emph{much} higher compared to \texttt{\tbs{}some}! +Proving that any value out of a defined set is fulfilling a condition is in my understanding way easier than proving that either \texttt{\tbs{}all} or even exactly \texttt{\tbs{}one} does so. + +It is also worth noting that usability extends far beyond the showcased example. +It would be thinkable to use those keywords outside of a reusable and non-redundant code design and just use them "in-line". +This also means that an introduction of a "named property" would still be required to achieve the goals showcased throghout this section. +That's why I mentioned that the need to have some kind of "dumb" macro, which would make it possible to assign a name to this epsilon-term, might still arise. +I have to investigate how I could utilize the already implemented (within KeY) notion of \emph{ghost variables}. + +Luckily an already implemented function of KeY could be used, modified, or at least used as a foundation for the proposed functionality. +The name of the class is \texttt{IfExThenElse} which one can use using the JML operator \texttt{\tbs{}ifEx}. +If we reference the \hreffn{http://i12www.ira.uka.de/~key/download/nightly/api/}{documentation for this class}, we can see some description on how to use it + +\[ + \mathrm{\tbs{}ifEx\ } i; (\phi)\ \mathrm{\tbs{}then\ } (t_1)\ \mathrm{\tbs{}else\ } (t2) +\] + +This conditional operator \texttt{\tbs{}ifEx} will check an integer logic variable $i$, which occurs in bound form within a formula $\phi$ and a term $t_1$, and proceed with term $t_1$ or $t_2$ respective of whether the bound variable can fulfull the formula $\phi$ for \emph{some} value. + +An implementation could therefore be possible using something like this pseudo code snippet: + +\begin{minted}{java} +/*@ def minScore = + @ (\ifEx int score; + @ (\exists int i; 0<=i && i<10; score == scores[i]) + @ && (\forall int i; 0<=i && i<10; score <= scores[i]) + @ \then + @ return score + @ \else + @ return None + @ ); + @*/ +//@ ensures newScore <= \old(minScore) ==> (\result == 0); +\end{minted} + +Note that in this example some value gets "returned". +This is probably not something you would want to achieve in KeY. +We wanted to describe the \emph{property} of a minimal score, not have a concrete value fulfilling this property. +This could also be something some kind of ghosting variable could achieve, but I would need to investigate this further. + +For the time being, one could inline this whole concept and possibly have a working example, though this would not necessarily improve either readability or code reusage, but definitely increase versatility and expressiveness. + +\begin{minted}{java} +/*@ ensures + @ (\ifEx int minScore; + @ (\exists int i; 0<=i && i<10; minScore == scores[i]) + @ && (\forall int i; 0<=i && i<10; minScore <= scores[i]) + @ \then + @ newScore <= minScore ==> (\result == 0) + @ \else + @ \result != 0 + @ ); + @*/ +\end{minted} + +Note however that I noticed the \texttt{\tbs{}else} branch is not really doing what it should be. +The else part doesn't handle the case of the \texttt{newScore} being higher than the minScore! +Instead it is handling the case when \emph{no} \texttt{minScore}, with the property of being an element in the \texttt{scores} array, as well as being the smallest element in this array, exists! +So in this case this would mean that our high score table is empty. +So this branch should either throw some kind of error, or rather make sure the ensures doesn't evaluate to true in that case, if this behaviour is not allowed, or if this is allowed, handle this case differently. +In case it isn't allowed to have an empty high score table, the example should be like follows + +\begin{minted}{java} +/*@ ensures + @ (\ifEx int minScore; + @ (\exists int i; 0<=i && i<10; minScore == scores[i]) + @ && + @ (\forall int i; 0<=i && i<10; minScore <= scores[i]) + @ \then + @ newScore <= minScore ==> (\result == 0) + @ \else + @ false + @ ); + @*/ +\end{minted} + +The main difficulty of this approach is the handling of the bound variable, the way of returning the notion of the fulfilling value to the caller, as in the notion of a value matching the property description, as well as handling the case of no value fulfilling the formula. + +In my opinion one could either use some sort of \texttt{null} value, or some sort of an \texttt{option} type. +With the \texttt{null} value, the "caller" would be in need of some kind of checking if such a \texttt{null} value has been returned. +With the \texttt{option} type could lift this burden from the user and put it on the compiler/runtime/etc. +The option type is a commonly used type in the programming language rust. +In this context the generic option type, initialized with a concrete type, either holds an instance of the specified type, or it holds the \emph{nothing} value. +Therefore one calls a mehtod on the option type either returning the instance of the specified type, or it raises and exception. +It would be interesting to investigate if this kind of behaviour would benefit this cause. + +\subsection{Conclusion} + +I think it might well be necessary to employ both proposed solutions together. +As I mentioned, defining and implementing some kind of epsilon-terms is useful in itsefl as it would greatly increase KeY, JavaDL, etc. in terms of versatility and expressiveness. +It would however not improve the original points of critique, namely redundancy and low readability. +To do that one would have to be able to \emph{name} a property, so it can be reused at multiple code points and upon finding an error, or edge case within a property definition, being able to change it in one centralized place and being sure that no other code point is in need of modification. +This would therefore raise the need of some kind of naming, which could be either solved by some kind of ghosting variable, or some simplistic macro handling. + +\newpage + +\section{Work Packages} + +I think the work lying ahead of me is contained withing the following work subjects. + +\begin{enumerate} + \item Research how \texttt{\tbs{}ifEx} is implemented within JavaDL and/or KeY, in order to be able to implement something smilar myself. + This should teach me all I need in terms of which source files are linked together or are standing in relation to one another, as well as how the different parts play together to create something that KeY can use for constructing a proof. + Try implementing or extending some placeholder functionality in order to get a feel for it. + + \item Research how I can implement the aforementioned epsilon substitution method. + Possibly research how such a notion is implemented in Java in general, or other programming languages that serve the intent of proof construction or proving code correctness more, like e.g. functional programming languages like Haskell. + + \item Research how ghosting variables could be used to achieve the wanted effect. + If this is not feasible, I would have to think about employing some kind of macros. + + \item Research how other programming languages implement macro handling, as well as to what extent. + This would greatly improve the understanding of whether this task, even if it only serves the purpose of naming the properties, is as easy as employing a preprocessor, or if some more intricate handling is necessary. + + \item Research which parts are implemented within KeY itself and which are implemented within JavaDL. + This will greatly help my understanding of the underlying working mechanisms of KeY, how they work together to construct proofs, etc. + + \item Possibly implement a minimal working example using \texttt{\tbs{}ifEx} to see in which cases it is lacking, or if it is already sufficient compared to the expected behaviour of a (blackbox implementation) \texttt{\tbs{}some}. + If not, I would have to manually implement the aforementioned keywords. + Therefore the goal of this task would be to determine if it would be feasible to embed the \texttt{\tbs{}ifEx} into a \texttt{\tbs{}some} keywoard or if a groud-up approach is necessary. + + \item Determine (using this minimal working example) what the true goal to be achieved through this thesis is, to have a concrete expectation horizon. + + \item Implement \texttt{some} with a minimal scope of functionality, i.e. a minimal working example. + According to how easy/difficult this task is, it is determined if implementation of \texttt{one} and/or \texttt{all} is workable within the given 6 months timeframe. + + \item Implement some kind of naming mechanism for the property definition. + + \item Construct multiple usage examples to demo and test the new functionality. + + \item Write extensive tests and also theoretically ground the approach and implementation to ensure issue-free usage. + + \item Document the implementation as well as the whole process to maintain reproducability. + + \item Write the thesis itself. + +\end{enumerate} + +\section{Schedule} + +I would estimate the amount of work needed to take (almost) all of these points to completion to be workable within the given timeframe of the thesis, namely 6 months. +I will expect to write the documentation as well as snippets of sections of the final thesis during the whole duration. +I will also expect to have the finalization of the thesis as well as the presentation take 6 weeks or more by themselves. +Apart from that I will mainly focus on finishing the rough research part as fast as possible, in order for me to determine wheter a complete implementation from scratch is needed or not. +Note however that this is subject to great fluctuation as well as change, as I can't really estimate the amount of work, further research, implementation and documentation that needs to be done. +Also note that for some tasks a non-sequential completion can be possible. + +\section{Challenges} + +When trying to implement this new token \texttt{\tbs{}some}, I encountered many hurdles. +Especially since some things, in particular \texttt{\tbs{}ifEx}, have some special quirks, limitation and/or boundaries in KeY at the time of writing my thesis, it took quite some time to get behind of all the underlying behaviour and inner workings of the code base, in order to ensure a clean implementation of the wanted token. + +\subsubsection{\texttt{\tbs{}some} as a quantifier} +First of all the question arose, in what form this token should be incorporated into the KeY codebase. +I decided to implement it as an extension of a collection of quantifiers withing KeY. + +Up to this point, the quantifiers available through JML were +\begin{itemize} + \item \texttt{\tbs{}forall} + \item \texttt{\tbs{}exists} + \item \texttt{\tbs{}min} + \item \texttt{\tbs{}max} + \item \texttt{\tbs{}sum} + \item \texttt{\tbs{}num\_of} +\end{itemize} + +By extending this collection of tokens with a new token \texttt{\tbs{}some}, we can utilize the generalized methods for the so called \emph{spec-quantified expressions}, that follow the syntax \texttt{LPAREN quantifier (boundvarmodifiers)? quantifiedvardecls SEMI (expression SEMI)? expression RPAREN}. +This means we can write a some statement the following way: + +\begin{minted}{java} +/*@ ensures (\some T quantifiedVariable; property; defaultValue) > someValue */ +\end{minted} + +In spoken speech form this wouuld mean that \emph{some} \texttt{quantifiedVariable} of type \texttt{T} defined by its \texttt{property} is greater than \texttt{someValue}. +If there is no \texttt{quantifiedVariable} of type \texttt{T} with the specified \texttt{property}, the \texttt{defaultValue} is returned instead and checked against it being greater than \texttt{someValue}. + +Furthermore the following holds true + +\begin{minted}{text} +(\some T var; (property); (defaultValue)) + +<==> + +(\ifEx T var; (property); \then (var) \else (defaultValue)) +\end{minted} + +Because of the somewhat unsual use of the second term for the \texttt{defaultValue}, it imposes some problems on the implementation +% TODO: elaborate + +\texttt{\tbs{}one} could also be implemented like this + +\begin{minted}{text} +(\one T var; (property); (defaultValue)) + +<==> + +(\ifEx + T var; + ( + property + && + (\forall T var2; + (property); + var==var2 + ) + ) + \then + (var) + \else + (defaultValue) +) + +<==> + +(\some T var; + ( + property + && + (\forall T var2; + (property); + var==var2 + ) + ); + defaultValue +) +\end{minted} + + +% \begin{verbatim} +% y = a.m() +% [...] +% await y? +% [...] +% \end{minted} +% +% \begin{figure} +% +% \includegraphics[page=124,width=\textwidth,trim=35 80 25 110,clip]{Presentation_final_slides.pdf} +% +% \caption{Example global MHP graph snippet showcasing direct MHP \cite{MHPA_ABC}} +% \label{fig:mhp-graph-big-direct} +% \end{figure} + +%\bibliographystyle{plain} +%% add the bibliography you want to use in the file below +%% you do not need to create bibtex entries by your self, +%% a good source is https://dblp.uni-trier.de (use the format without crossreferences) +%\bibliography{proposal} + +\end{document}