Added intrdocution

diff --git a/report/formal.pdf b/report/formal.pdf
index 8e61024..6338113 100644 (file)
Binary files a/report/formal.pdf and b/report/formal.pdf differ

diff --git a/report/formal.tex b/report/formal.tex
index 74a870f..d220fe4 100644 (file)
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -136,8 +136,8 @@ the implementation of a real-life task.\\
 Such Design by Contracts have been incoorporated into several programming languages, such as Java (by the
 Java Modelling Language JML \cite{JML}) and C and \CC (for example, by the Larch project \cite{Larch}), in
 one way or the other. Instrumenting the source code by requiring pre-conditions and ensuring post-conditions,
 Such Design by Contracts have been incoorporated into several programming languages, such as Java (by the
 Java Modelling Language JML \cite{JML}) and C and \CC (for example, by the Larch project \cite{Larch}), in
 one way or the other. Instrumenting the source code by requiring pre-conditions and ensuring post-conditions,

-allow a formal verification of the implemented algorithm. Further, additional provers such as the KeY-system
-investigate this formal correctness of program code.\\
+allow a formal verification of the implemented algorithm. Further, additional verification tools such as the
+KeY-system \cite{KeY}, that investigates this formal correctness of program code.\\

 
 Recently, at RISC the algorithm language {\rm RISCAL} \cite{Schreiner} has been developed.
 {\rm RISCAL} allows to
 
 Recently, at RISC the algorithm language {\rm RISCAL} \cite{Schreiner} has been developed.
 {\rm RISCAL} allows to


@@ -171,40 +171,40 @@ Our presentation consolidates the results presented in \cite{Schreiner, Schreine
 main elements of RISCAL are summarized as follows.\\
 \noindent\rule{\textwidth}{1pt}
 \small
 main elements of RISCAL are summarized as follows.\\
 \noindent\rule{\textwidth}{1pt}
 \small

-\textit{\textbf{System} The RISCAL specification language is based on a statically typed variant of first order
+\textbf{System} The RISCAL specification language is based on a statically typed variant of first order

   predicate logic. On the one hand, it allows to develop mathematical theories [...];
   on the other hand, it also enables the specification of
   algorithms [...]. The lexical syntax of the language includes Unicode characters for common mathe-
   matical symbols; these may be entered in the {\rm RISCAL} editor via ASCII shortcuts; e.g., the character ∀
   is entered by first typing the text forall and then pressing the keys \texttt{<Ctrl>} and \texttt{\#}
   predicate logic. On the one hand, it allows to develop mathematical theories [...];
   on the other hand, it also enables the specification of
   algorithms [...]. The lexical syntax of the language includes Unicode characters for common mathe-
   matical symbols; these may be entered in the {\rm RISCAL} editor via ASCII shortcuts; e.g., the character ∀
   is entered by first typing the text forall and then pressing the keys \texttt{<Ctrl>} and \texttt{\#}

-  simultaneously.}\\~\\
-\textit{\textbf{Language} {\rm RISCAL} specifications consist of declarations of the following kinds of
-  entitities}\\~\\
-\textit{\textbf{Types} type $I = T$ introduces a named type $I$ defined by the type expression $T$;
+  simultaneously.\\~\\
+\textbf{Language} {\rm RISCAL} specifications consist of declarations of the following kinds of
+  entitities\\~\\
+\textbf{Types} type $I = T$ introduces a named type $I$ defined by the type expression $T$;

   types include booleans, integers, sets, tuples, records, arrays, and maps (partial functions).
   All types are \emph{finite}, e.g., for integer constants $N$ and $M$ with $N ≤ M$ the type $\mathrm{Z}[N,M]$
   denotes the type of all integers in the interval $[N, M]$ while \texttt{Array}$[N,T]$ denotes the type of
   all arrays of length $N ≥ 0$ with elements of type $T$ . Recursive (algebraic) data types (whose values are
   terms of a finite depth $N ≥ 0$) may be introduced by a declaration
   types include booleans, integers, sets, tuples, records, arrays, and maps (partial functions).
   All types are \emph{finite}, e.g., for integer constants $N$ and $M$ with $N ≤ M$ the type $\mathrm{Z}[N,M]$
   denotes the type of all integers in the interval $[N, M]$ while \texttt{Array}$[N,T]$ denotes the type of
   all arrays of length $N ≥ 0$ with elements of type $T$ . Recursive (algebraic) data types (whose values are
   terms of a finite depth $N ≥ 0$) may be introduced by a declaration

-  \texttt{rectype}$(N) T = c(T 1 ,...,T n )$\texttt{ | ...}.}\\~\\
-\textit{\textbf{Constants} \texttt{val }$I:\mathbb{N}$ introduces an unspecified natural number constant
+  \texttt{rectype}$(N) T = c(T 1 ,...,T n )$\texttt{ | ...}.\\~\\
+\textbf{Constants} \texttt{val }$I:\mathbb{N}$ introduces an unspecified natural number constant

   $I$ while \texttt{val} $I:T = E$ introduces a constant $I$ of type $T$ which is explicitly defined by a
   term $E$. Terms can be composed from a rich variety of built-in functions and quantifiers, e.g. the term
   ( ∑ \texttt{x}:$\mathbb{N}$\texttt{[N]} with \texttt{x\%2=0. x·x})
   $I$ while \texttt{val} $I:T = E$ introduces a constant $I$ of type $T$ which is explicitly defined by a
   term $E$. Terms can be composed from a rich variety of built-in functions and quantifiers, e.g. the term
   ( ∑ \texttt{x}:$\mathbb{N}$\texttt{[N]} with \texttt{x\%2=0. x·x})

-  denotes the sum of the squares of all odd natural numbers less than equal $N$}\\~\\
-\textit{\textbf{Functions and Predicates} \texttt{fun $I$(...): $T=E$} introduces a function $I$ with result
+  denotes the sum of the squares of all odd natural numbers less than equal $N$\\~\\
+\textbf{Functions and Predicates} \texttt{fun $I$(...): $T=E$} introduces a function $I$ with result

   type $T$ ; the result value is defined by expression $E$ of type $T$; correspondingly,
   \texttt{pred} $I(...) ⇔ F$ defines a predicate $I$, i.e., a Boolean-valued function whose result
   is defined by formula $F$ (an expression of type \texttt{Bool}). Formulas can be written in a notation
   that is close to typical mathematical practice, e.g.,
   \texttt{(∀x:$\mathbb{N}$[N],y:$\mathbb{N}$[N]. x ≤ y ⇒ ∃z:Nat. z ≤ y ∧ x+z = y)} is such a formula.
   type $T$ ; the result value is defined by expression $E$ of type $T$; correspondingly,
   \texttt{pred} $I(...) ⇔ F$ defines a predicate $I$, i.e., a Boolean-valued function whose result
   is defined by formula $F$ (an expression of type \texttt{Bool}). Formulas can be written in a notation
   that is close to typical mathematical practice, e.g.,
   \texttt{(∀x:$\mathbb{N}$[N],y:$\mathbb{N}$[N]. x ≤ y ⇒ ∃z:Nat. z ≤ y ∧ x+z = y)} is such a formula.

-}\\~~\\
-\textit{\textbf{Theorems} \texttt{theorem }$I$ ⇔ $F$ introduces a Boolean constant $I$ whose value is
+\\~~\\
+\textbf{Theorems} \texttt{theorem }$I$ ⇔ $F$ introduces a Boolean constant $I$ whose value is

   defined by a formula $F$; this declaration asserts that the value of $I$ is \texttt{true}, i.e., that
   $F$ is valid. Likewise \texttt{theorem } $I(...)$ ⇔ $F$ introduces a predicate $I$ defined by formula
   $F$; this declaration asserts that $F$ is valid for all possible parameter values, i.e., $F$ is
   defined by a formula $F$; this declaration asserts that the value of $I$ is \texttt{true}, i.e., that
   $F$ is valid. Likewise \texttt{theorem } $I(...)$ ⇔ $F$ introduces a predicate $I$ defined by formula
   $F$; this declaration asserts that $F$ is valid for all possible parameter values, i.e., $F$ is

-  implicitly universally quantified.}\\~\\
-\textit{\textbf{Procedures} \texttt{proc} $I$(...):$T$ \{ $C$; \texttt{return} $E$; \} introduces a procedure
+  implicitly universally quantified.\\~\\
+\textbf{Procedures} \texttt{proc} $I$(...):$T$ \{ $C$; \texttt{return} $E$; \} introduces a procedure

   $I$ with result type $T$ . A procedure is a function whose result value is determined by the
   execution of command $C$; this establishes a context (determined by the values of modifiable
   variables in the procedure) in which the value of expression $E$ is evaluated to denote the
   $I$ with result type $T$ . A procedure is a function whose result value is determined by the
   execution of command $C$; this establishes a context (determined by the values of modifiable
   variables in the procedure) in which the value of expression $E$ is evaluated to denote the


@@ -213,7 +213,7 @@ main elements of RISCAL are summarized as follows.\\
   invariant $F$ to indicate that formula $F$ is \texttt{true} before and after every iteration of the loop;
   the annotation decreases $E$ indicates that the value of the termination measure $E$ (a natural number
   expression) is decreased in every iteration. A command assert $F$ indicates that formula $F$ is true
   invariant $F$ to indicate that formula $F$ is \texttt{true} before and after every iteration of the loop;
   the annotation decreases $E$ indicates that the value of the termination measure $E$ (a natural number
   expression) is decreased in every iteration. A command assert $F$ indicates that formula $F$ is true

-  when the command is executed.}\\
+  when the command is executed.\\

 \noindent\rule{\textwidth}{1pt}
 
 \normalsize
 \noindent\rule{\textwidth}{1pt}
 
 \normalsize


@@ -224,7 +224,20 @@ and further divide the tasks into several threads to enable parallelism of the c
 particular off, when considering large scale inputs, as the growth of the considered inputs can be exponential.
 With the ``Operation'' one chooses the algorithm that is actually considered. The lower half of the right hand
 side is the logfile of the analysis, that points out where errors, such as syntactical faults, but also
 particular off, when considering large scale inputs, as the growth of the considered inputs can be exponential.
 With the ``Operation'' one chooses the algorithm that is actually considered. The lower half of the right hand
 side is the logfile of the analysis, that points out where errors, such as syntactical faults, but also

-invalid post-conditions or invariants are reported.
+invalid post-conditions or invariants are reported.\\
+
+We want to emphasize the scope of RISCAL. It is a powerful way to formulate algorithms, their invariants and
+can be used to reason about correctness. It is independent of concrete implementation (where side effects such
+as variable overflow could occur, and produce wrong results even if the algorithm is correct on an infinite
+domain), and will give the user a feedback, whether his realization of the algorithm is valid in principle.
+The verification still relies on finite domains, due to obvious restrictions. Still, the evidence is the
+counting part, and the system RISCAL should be the tool of choice for getting started with the formulation
+of complex algorithms.\\
+
+With this (way too short) introduction, we want to already leave this account on RISCAL, and refer the
+interested reader to \cite{Schreiner, SchreinerBrunhuemerFuerst, Brunhuemer}. Instead we will now continue
+by focusing our attention to concrete applications. First, we have to recall some mathematical and
+number theoretic preliminaries.

 
 \section{Mathematical and Number Theoretic Preliminaries}
 Classic textbooks on number theory and finite fields are \cite{hardylittlewood,LidlNiederreiter}.
 
 \section{Mathematical and Number Theoretic Preliminaries}
 Classic textbooks on number theory and finite fields are \cite{hardylittlewood,LidlNiederreiter}.


@@ -410,7 +423,7 @@ The integer root problem, is the problem of
 \end{equation}
 \end{itemize}
 There is an obvious, ``brute-force'' algorithm available, which proceeds by initializing $m$ by 1,
 \end{equation}
 \end{itemize}
 There is an obvious, ``brute-force'' algorithm available, which proceeds by initializing $m$ by 1,

-and increment $m$ until condition \eqref{eq:sqr} is fulfilled. A slightly more sophisticated algorithm
+and incrementing $m$ until condition \eqref{eq:sqr} is fulfilled. A slightly more sophisticated algorithm

 would proceed as follows.
 \begin{algorithm}[H]
 \begin{algorithmic}[1]
 would proceed as follows.
 \begin{algorithm}[H]
 \begin{algorithmic}[1]


@@ -694,6 +707,9 @@ Oxford University Press, 6. edition. 2008.
 \text{The Java Modelling Language (JML)} Home page, February
 2013 \url{http://www.jmlspecs.org}
 
 \text{The Java Modelling Language (JML)} Home page, February
 2013 \url{http://www.jmlspecs.org}
 

+\bibitem{KeY}
+\text{The KeY Project} Homepage, February 2018 \url{https://www.key-project.org}
+

 \bibitem{Larch}
 \text{The Larch System} Home page, May 2017
 \url{https://www.cs.cmu.edu/afs/cs/project/larch/www/home.html}
 \bibitem{Larch}
 \text{The Larch System} Home page, May 2017
 \url{https://www.cs.cmu.edu/afs/cs/project/larch/www/home.html}