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
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{\#}
- 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
- \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})
- 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.
-}\\~~\\
-\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
- 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
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
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}.
\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]
\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}
projects / cfuerst / formal-numbers.git / commitdiff