Next final version; Excluding the working example demo for now because it is not finished yet.
This commit is contained in:
parent
e211ed185d
commit
8d17f39761
1202
proposal.pdf
1202
proposal.pdf
File diff suppressed because it is too large
Load Diff
179
proposal.tex
179
proposal.tex
|
|
@ -95,6 +95,8 @@ pdfa=false % we disable pdf/a mode to achieve easier compilation compatibility
|
|||
|
||||
\newcommand{\hreffn}[2]{\href{#1}{#2}\footnote{#1}}
|
||||
|
||||
\newcommand{\tbs}{\textbackslash}
|
||||
|
||||
\title{Proposal}
|
||||
\subtitle{%
|
||||
Thesis\\
|
||||
|
|
@ -111,7 +113,8 @@ Supervisor: Lukas Grätz
|
|||
|
||||
\section{Motivation}
|
||||
|
||||
To explain the necessity of the following elaborations, as well as to ground the motivation, I will use the following java class \texttt{HighScoreTable}, which implements the notion of a high score table.
|
||||
To explain the necessity of the following elaborations, as well as to ground the motivation, I will use the following java class \texttt{HighScoreTable}, 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 {
|
||||
|
|
@ -186,10 +189,11 @@ public class HighSoreTable {
|
|||
* 1 if otherwise
|
||||
*/
|
||||
//@ requires newScore >= 0;
|
||||
//@ def lowerThanMin(score) =
|
||||
(\forall int i; 0<=i && i<10;
|
||||
score <= \old(scores[i])
|
||||
);
|
||||
/*@ def lowerThanMin(score) =
|
||||
@ (\forall int i; 0<=i && i<10;
|
||||
@ score <= \old(scores[i])
|
||||
@ );
|
||||
*/
|
||||
//@ ensures lowerThanMin(newScore) ==> (\result == 0);
|
||||
// [...]
|
||||
public int addScore(int newScore) {
|
||||
|
|
@ -204,20 +208,17 @@ For implementing this, I could use the concept of a preprocessor, which simply e
|
|||
So for example
|
||||
|
||||
\begin{minted}{java}
|
||||
//@ def lowerThanMin(score) =
|
||||
// (\forall int i; 0<=i && i<10;
|
||||
// score <= \old(scores[i])
|
||||
// );
|
||||
/*@ 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}
|
||||
//@ def lowerThanMin(score) =
|
||||
// (\forall int i; 0<=i && i<10;
|
||||
// score <= \old(scores[i])
|
||||
// );
|
||||
//@ ensures (\forall int i; 0<=i && i<10; newScore <= \old(scores[i])); ==> (\result == 0);
|
||||
\end{minted}
|
||||
|
||||
|
|
@ -230,10 +231,11 @@ One would need to manually search \& replace the whole code, in other words expa
|
|||
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])
|
||||
// );
|
||||
/*@ def lowerThanMin(int score) =
|
||||
@ (\forall int i; 0<=i && i<10;
|
||||
@ score <= \old(scores[i])
|
||||
@ );
|
||||
*/
|
||||
//@ ensures lowerThanMin(newScore) ==> (\result == 0);
|
||||
\end{minted}
|
||||
|
||||
|
|
@ -247,51 +249,58 @@ or alternatively, to serve the lambda notion more
|
|||
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)
|
||||
// );
|
||||
/*@ 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 the description of the \texttt{ensures} is not as intuitive, as it solemnly uses FOL.
|
||||
Therefore instead of defining a \emph{method} on \emph{how} it can be determined if a 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 given score to.
|
||||
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])
|
||||
// );
|
||||
/*@ 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{some}.
|
||||
Other possible keywords with a similar notion would be \texttt{all}, as well as \texttt{one}.
|
||||
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{one} selects \emph{the one} value fulfilling the specified conditional property.
|
||||
\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{some} selects \emph{some} value non-deterministically, which fulfills a specified conditional property.
|
||||
\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{all} in turn selects \emph{all} values fulfilling the specified conditional property.
|
||||
\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{some}.
|
||||
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.
|
||||
|
|
@ -306,10 +315,10 @@ The epsilon calculus can express first-order-logic (FOL), but not the other way
|
|||
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, would be the \texttt{one} keyword, as that is the notion of the \emph{definite description}.
|
||||
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.
|
||||
|
||||
I would also rank the difficulty of the \texttt{all} keyword between the two aforementioned as I would still need to deal with the epsilon calculus but not with the non-deterministic part.
|
||||
\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".
|
||||
|
|
@ -318,28 +327,29 @@ That's why I mentioned that the need to have some kind of "dumb" macro, which wo
|
|||
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{\textbackslash{}ifEx}.
|
||||
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{\textbackslash{}ifEx\ } i; (\phi)\ \mathrm{\textbackslash{}then\ } (t_1)\ \mathrm{\textbackslash{}else\ } (t2)
|
||||
\mathrm{\tbs{}ifEx\ } i; (\phi)\ \mathrm{\tbs{}then\ } (t_1)\ \mathrm{\tbs{}else\ } (t2)
|
||||
\]
|
||||
|
||||
This conditional operator \texttt{\textbackslash{}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.
|
||||
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
|
||||
// );
|
||||
/*@ 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}
|
||||
|
||||
|
|
@ -351,16 +361,17 @@ This could also be something some kind of ghosting variable could achieve, but I
|
|||
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; score == scores[i])
|
||||
// &&
|
||||
// (\forall int i; 0<=i && i<10; score <= scores[i])
|
||||
// \then
|
||||
// newScore <= minScore ==> (\result == 0)
|
||||
// \else
|
||||
// \result != 0
|
||||
// );
|
||||
/*@ 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}
|
||||
|
||||
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.
|
||||
|
|
@ -388,7 +399,7 @@ This would therefore raise the need of some kind of naming, which could be eithe
|
|||
I think the work lying ahead of me is contained withing the following work subjects.
|
||||
|
||||
\begin{enumerate}
|
||||
\item Research how \texttt{\textbackslash{}ifEx} is implemented within JavaDL and/or KeY, in order to be able to implement something smilar myself.
|
||||
\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.
|
||||
|
||||
|
|
@ -404,51 +415,35 @@ I think the work lying ahead of me is contained withing the following work subje
|
|||
\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{\textbackslash{}ifEx} to see in which cases it is lacking, or if it is already sufficient.
|
||||
\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.
|
||||
Specifically, I will roughly estimate the time it would take for each task to complete.
|
||||
Note however that this is subject to great fluctuation as well as change.
|
||||
Also note that the following listing does not imply the tasks to be completed sequentially.
|
||||
|
||||
\begin{enumerate}
|
||||
\item 2 weeks
|
||||
|
||||
\item 2-3 weeks.
|
||||
|
||||
\item 1-2 weeks
|
||||
|
||||
\item 1 weeks
|
||||
|
||||
\item 1-2 weeks
|
||||
|
||||
\item 1 week
|
||||
|
||||
\item 3 weeks
|
||||
|
||||
\item 2 weeks
|
||||
|
||||
\item 2 weeks
|
||||
|
||||
\item During the whole duration
|
||||
|
||||
\item Also during the whole duration + ~6 weeks?
|
||||
\end{enumerate}
|
||||
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.
|
||||
|
||||
% \begin{verbatim}
|
||||
% y = a.m()
|
||||
|
|
|
|||
Loading…
Reference in New Issue