Added information about RISCAL

diff --git a/report/formal.pdf b/report/formal.pdf
index a2eef63..8e61024 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 f8daff9..74a870f 100644 (file)
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -167,6 +167,56 @@ to formulate the considered algorithms in a certain `\textit{programming languag
 that is independent of concrete implementations in programming languages, and verifies the syntactic
 correctness.\\
 
+Our presentation consolidates the results presented in \cite{Schreiner, SchreinerBrunhuemerFuerst}, where the
+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
+  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$;
+  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
+  $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
+  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
+  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
+  $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
+  result value. Commands support the usual algorithmic constructs like variable assignments,
+  command sequences, and various forms of conditionals and loops. Loops may be annotated by
+  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.}\\
+\noindent\rule{\textwidth}{1pt}
+
+\normalsize
 As for the analysis of the considered algorithms, the right hand side is split into a ``parametrization''
 of the analysis, where the user can choose between deterministic and non-deterministic analysis, certain
 default values that bound the range of considered values, whether the execution should be verbose or silent,