\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}
\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}
\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}
\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}
\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.\\
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
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
$$
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}.
(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<e ∧ isPrime(p) ∧ e%p = 0;
+theorem MinOfSetExists() ⇔ ∀s:Set[nat] with s ≠ ∅[nat]. ∃e:nat. 0 ≤ e ∧ e ≤ MAX ∧ e ∈ s ∧ ∀m ∈ s. e ≤ m;
+\end{xverbatim}
+\caption{Theorems for Set-Based Sieve of Erathostenes Algorithm in RISCAL}
+\label{fig:setsieve}
+\end{figure}
\subsection{The Sieve of Erathostenes II}
\begin{thebibliography}{9}
+\bibitem{Brunhuemer}
+A. Brunhuemer. \textit{Validating the Formalization of Theories and Algorithms of Discrete
+ Mathematics by the Computer-Supported Checking of Finite Models}. Bachelor thesis, Research
+Institute for Symbolic Computation (RISC), Johannes Kepler University, Austria, 2017.
+
\bibitem{FuriaMeyer}
C. A. Furia and B. Meyer. \textit{Inferring Loop Invariants Using Postconditions}
A. Blass, N. Dershowitz, and W. Reisig (Eds.): Gurevich Festschrift, LNCS 6300, pp. 277–300, 2010.
R. Lidl and H. Niederreiter. \textit{Introduction to finite fields and their applications}.
Cambridge University Press, 1986.
+\bibitem{Ritirc}
+D. Ritirc. \textit{Formally Modeling and Analyzing Mathematical Algorithms with Software
+ Specification Languages \& Tools}, Master's thesis, RISC, Johannes Kepler University, Linz, Austria, 2016.
+
+\bibitem{SchreinerBrunhuemerFuerst}
+W. Schreiner, A. Brunhuemer, C. F\"urst. \textit{Teaching the Formalization of Mathematical Theories and
+ Algorithms via the Automatic Checking of Finite Models}. Post-Proceedings ThEdu'17, Pedro Quaresm and Walther Neuper (ed.), Proceedings of Theorem proving components for Educational software, 6 August 2017, Gothenburg, Sweden, at CADE26, Electronic Proceedings in Theoretical Computer Science (EPTCS) , pp. 1-20. 2018. ISSN 2075-2180.
+
\bibitem{Schreiner}
W. Schreiner. \textit{The RISC Algorithm Language (RISCAL), Tutorial and Reference}.
Research Institute for Symbolic Computation (RISC) Linz, 2017.
+\bibitem{Schreiner2}
+W. Schreiner. \textit{The RISC ProofNavigator: A Proving Assistant for Program Verification in the
+ Classroom}, Formal Aspects of Computing 21(3), pp. 277--291, doi:10.1007/s00165-008-0069-4, 2009.
+
\end{thebibliography}
\end{document}
projects / cfuerst / formal-numbers.git / commitdiff