From: Christoph Fuerst Date: Sun, 28 Jan 2018 15:39:23 +0000 (+0100) Subject: Added information about RISCAL X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=070432b4fd7c65472a36ed6cfe46aed4cdeec262;p=cfuerst%2Fformal-numbers.git Added information about RISCAL --- diff --git a/report/formal.pdf b/report/formal.pdf index a2eef63..8e61024 100644 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 --- 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{} 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,