From: Christoph Fuerst Date: Sun, 14 Jan 2018 10:14:45 +0000 (+0100) Subject: Added section on RISCAL, formulated algorithms and Theorems X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=e2dd2410ab6f5d9316209f5fb8f2ecd0bfe1d9d7;p=cfuerst%2Fformal-numbers.git Added section on RISCAL, formulated algorithms and Theorems --- diff --git a/report/formal.pdf b/report/formal.pdf index a8fa64f..a2eef63 100644 Binary files a/report/formal.pdf and b/report/formal.pdf differ diff --git a/report/formal.tex b/report/formal.tex index 61ce817..f8daff9 100644 --- a/report/formal.tex +++ b/report/formal.tex @@ -1,7 +1,10 @@ \documentclass[a4paper,10pt]{scrartcl} -\usepackage[utf8x]{inputenc} \usepackage{lmodern} \usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{newunicodechar} +\input{unicodechars} + \usepackage{verbatim} \usepackage{amsmath} \usepackage{amsthm} @@ -11,6 +14,22 @@ \usepackage{listings} \usepackage{xcolor} \usepackage{textcomp} +\usepackage{graphicx} +% eptcs customization +\providecommand{\event}{ThEdu'17 Post-Proceedings} % Name of the event you are submitting to +%\usepackage{breakurl} % Not needed if you use pdflatex only. +\usepackage{underscore} % Only needed if you use pdflatex. + +% miscellaneous packages +\usepackage{csquotes} +\usepackage{verbatim} +\usepackage[nounderscore]{syntax} +\usepackage{graphicx} +\usepackage{amsmath} +\usepackage{amsthm} +\usepackage{amssymb} +\usepackage{mathbbol} + % \newtheorem{thm}{Theorem}[section] \newtheorem{cor}[thm]{Corollary} @@ -21,6 +40,9 @@ \newtheorem{ex}[thm]{Example} \theoremstyle{remark} \newtheorem{rem}[thm]{Remark} +\newenvironment{xgrammar}{\begin{quote}\begin{grammar}}{\end{grammar}\end{quote}} +\newenvironment{xverbatim}{\quote\verbatim}{\endverbatim\endquote} +\newenvironment{xprogram}{\quote\verbatim}{\endverbatim\endquote} \numberwithin{equation}{section} @@ -62,7 +84,9 @@ \usepackage[hidelinks]{hyperref} \newcommand{\CC}{C\nolinebreak\hspace{-.05em}\raisebox{.4ex}{\tiny\bf +}\nolinebreak\hspace{-.10em}\raisebox{.4ex}{\tiny\bf +}} \def\CC{{C\nolinebreak[4]\hspace{-.05em}\raisebox{.4ex}{\tiny\bf ++}}\,} - +\makeatletter +\def\verbatim@font{\scriptsize\ttfamily} +\makeatother %opening \title{Formalization of Two Algorithms arising in Number Theory} \author{Christoph F\"urst\qquad Wolfgang Schreiner\\ Research Institute for Symbolic Computation (RISC) Linz} @@ -92,13 +116,13 @@ formulated post-conditions are indeed valid. \section{Introduction} In mathematics and computer science, we are in position to design and implement algorithms, -that operate on certain inputs and compute outputs that satisfy certain constraints on the -input parameters. We have building blocks, that connect like a puzzle, and allow us to -compute the output without further justification. However, already the input domain -is often rather general, e.g. we deal with unbounded domains of values. Aesthethic -beauty in mathematics lies in its generality, this is, we try to formulate algorithms -and theorems in full generality, on the largest domain, such as the category of rings, -vector spaces and even more general constructions. Unfortunately, the price we pay for +that operate on certain inputs and compute outputs that satisfy certain constraints dependent on +the choice of input parameters. A complex cryptographic algorithm application consists of several +building blocks, that connect like a puzzle, and allow us to compute the desired output without further +justification. However, already the input domain is often rather general, e.g. we deal with +unbounded domains of values. Aesthethic beauty in mathematics lies in its generality, this is, +we try to formulate algorithms and theorems in full generality, on the largest applicable domain, such as +the category of rings, vector spaces and even more general constructions. Unfortunately, the price we pay for generality is that we have to apply more human insight in proving statements, and make it hard for the computer to formally verify statements and prove formal (partial) correctness.\\ @@ -115,7 +139,8 @@ one way or the other. Instrumenting the source code by requiring pre-conditions allow a formal verification of the implemented algorithm. Further, additional provers such as the KeY-system investigate 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 formulate an algorithm in pseudo-code, and deduce and verify certain properties of this pseudo-code. To that end, verification conditions, logical formulas, preconditions, postconditions and invariants are valitated at each step of execution. Still, {\rm RISCAL} is an algorithm formalization rather than @@ -125,6 +150,32 @@ a reasonable assumption, that counter-examples are expected at reasonable small are plenty of exceptions, and it is possible to construct certain examples where algorithms will fail at certain sizes of their inputs. +\section{RISCAL} +\begin{figure} +\centering +\includegraphics[width=0.87\textwidth]{RISCAL.png} +\caption{The RISCAL System} +\label{fig:RISCAL} +\end{figure} + + +We start by giving a brief overview of the RISCAL system. Starting the RISCAL system, we get a split screen +(as in Figure \ref{fig:RISCAL}), where the left half of the screen is essentially an editor, where +the algorithm can be typed in a certain +specification syntax. The RISCAL specification language encodes first order predicate logic. It allows +to formulate the considered algorithms in a certain `\textit{programming language like}' text-file, +that is independent of concrete implementations in programming languages, and verifies the syntactic +correctness.\\ + +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, +and further divide the tasks into several threads to enable parallelism of the computation. This pays in +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. + \section{Mathematical and Number Theoretic Preliminaries} Classic textbooks on number theory and finite fields are \cite{hardylittlewood,LidlNiederreiter}. Throughout this paper, let $\mathbb{N}$ denote the non-negative @@ -359,6 +410,36 @@ y > n \Leftrightarrow (x^2+z) > n \Leftrightarrow x^2+2x+1 > n \Leftrightarrow ( $$ hence we have shown $x^2\leq n < (x+1)^2$, and taking square roots shows the claim. \end{proof} +Equipped with that piece of insight, we are now in position to formulate the algorithm in the +RISCAL language. +\begin{figure}[t] +\begin{xverbatim} +val K: ℕ; +type nat = ℕ[K]; +//////////////////////////////////////////////////////////////////// +// Algorithm: Integer-Square-Root +//////////////////////////////////////////////////////////////////// +proc integerroot(a:nat): nat + ensures result^2 ≤ a ∧ a < (result+1)^2; +{ + var x:nat = 0; + var y:ℕ[(K+1)^2] = 1; + var z:ℕ[(K+1)^2] = 1; + + while y ≤ a do + invariant x^2 ≤ a ∧ y = x^2+z ∧ z = 2*x+1; + { + x=x+1; + z=z+2; + y=y+z; + } + + return x; +} +\end{xverbatim} +\caption{Integer Root Algorithm in RISCAL} +\label{fig:introot} +\end{figure} \subsection{The Sieve of Erathostenes I} We have described the algorithm for computing the set of prime numbers less equal $n$ in section \ref{sec:math}. @@ -423,6 +504,45 @@ In the beginning, the set $Q$ is not empty, but at each execution step, elements (as the set $\{s\in Q: \min(Q)|s\}$ is not empty), and therefore, the cardinality of $Q$ decreases. Therefore, the termination of the algorithm is a consequence of the fact that $|Q|$ decreases, and this descent can only be performed finitely often. +\begin{figure}[t] +\begin{xverbatim} +fun SetMin(s:Set[nat]): nat + requires s ≠ ∅[nat]; + ensures result ∈ s ∧ ∀e ∈ s. result ≤ e; + = choose m in s with ∀e in s. m ≤ e; + +proc SieveOfErathostenesSet(m:nat): Set[nat] + ensures ∀e:nat. e ≤ m ⇒ (e ∈ result ⇔ isPrime(e)); +{ + var start:Set[nat] := 2..m; + var ret:Set[nat] := ∅[nat]; + + while start ≠ ∅[nat] do + decreases |start|; + invariant start ⊆ 2..m ∧ ret ⊆ 2..m; + invariant ∀e ∈ ret. isPrime(e); + invariant start ≠ ∅[nat] ⇒ ∀e ∈ ret. e < SetMin(start); + invariant ∀e:nat. e ≤ m ∧ ¬(e ∈ start) ∧ isPrime(e) ⇒ e ∈ ret; + { + var locmi:nat = SetMin(start); + ret = ret ∪ {locmi}; + start = start \ ({locmi} ∪ { if divides(locmi,x) then x else locmi | x ∈ start}); + } + return ret; +} +\end{xverbatim} +\caption{Set-Based Sieve of Erathostenes Algorithm in RISCAL} +\label{fig:setsieve} +\end{figure} + +\begin{figure}[t] +\begin{xverbatim} +theorem PrimeDivisor() ⇔ ∀e:nat. (e > 1 ∧ ¬isPrime(e)) ⇒ ∃p:nat. p