From: Christoph Fuerst Date: Fri, 2 Feb 2018 07:48:53 +0000 (+0100) Subject: Added intrdocution X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;ds=sidebyside;p=cfuerst%2Fformal-numbers.git Added intrdocution --- diff --git a/report/formal.pdf b/report/formal.pdf index 8e61024..6338113 100644 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 --- 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, -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 @@ -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 -\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{} 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 @@ -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 - when the command is executed.}\\ + when the command is executed.\\ \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 -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}. @@ -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, -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] @@ -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} +\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}