stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered
tabsize=2, % sets default tabsize to 2 spaces
}
-\usepackage{hyperref}
+\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 ++}}}
the term \emph{divisor}, we say for $a,c\in\mathbb{Z}$,
that \emph{$a$ divides $c$}, and write $a|c$, if there is a number $b\in\mathbb{Z}$
such that $c = a\cdot b$. Every number $n\in\mathbb{N}$ has at least
-two divisors, a \emph{prime number} $p\in\mathbb{N}$ is a number $p$
-that has exactly two divisors, $1$ and $p$. Let now be given two numbers
+two divisors 1 and $n$, a \emph{prime number} $p\in\mathbb{N}$ is a number $p$
+that has exactly two divisors, 1 and $p$. Obviously, 1 divides every natural number,
+which we exclude by considering only \emph{proper divisors} greater 1.
+Let now be given two numbers
$a,b\in\mathbb{N}$. Among all divisors of two numbers $a$,$b$ there is a
unique \emph{greatest common divisor} of $a$ and $b$, denoted by $\gcd(a,b)$,
that is computed by the \emph{Euclidean algorithm}. The \emph{extended Euclidean algorithm}
Every natural number can be written as product of primes uniquely up to order.
\end{thm}
A constructive proof of the fundamental theorem is obtained, by showing that the
-smallest divisor $p_1$ of $n\in\mathbb{N}$ (with both, $n$ and $p_1$, greater than one)
+smallest proper divisor $p_1$ of $n\in\mathbb{N}$ (with both, $n$ greater than one)
is prime. An algorithm for computing the prime decomposition proceeds recursively considering
-$n/p_1$. This steps are performed until $n/(p_1\ldots p_k) = 1$.\\
+$n/p_1$. This steps are performed until $n/(p_1\ldots p_k) = 1$.
+
+\begin{lem}\label{lem:leastelemisprime}
+ Let $n$ be a natural number greater equal 2. Then, the least proper divisor of $n$ is a prime.
+\end{lem}
+\begin{proof}
+ We consider the set $D(n) := \{m\in \mathbb{N}: m|n\}$. Obviously, $D(n)$ is not empty (e.g.
+ $n\in D(n)$), and $D(n)\subseteq \mathbb{N}$. The natural numbers are well-ordered, hence
+ every non-empty subset of $\mathbb{N}$ has a least element. Denote this least element element by $n'$. If $n'$ is
+ prime, we are finished. On the other hand, if $n'$ is composite, say $n'=ab$ where $a,b>1$, then
+ $a,b < n'$ and
+ $$
+ a | n' \wedge n' | n \Rightarrow a | n
+ $$
+ contradicting the minimal property.
+\end{proof}
+
+
The first algorithm we will be concerned with the (more or less) opposite problem. Given a natural
number $n$, we are interested in answering the question:
\text{Describe the set }\, P(n) := \{p\in\mathbb{N}: 2 \leq p\leq n \wedge p \text{ is prime}\}.\tag{{\rm Q1}}
\end{equation}
The cardinality of the set $P$ is in classic textbooks referred by $\pi(n)$.
-The famous prime number theorem gives information about the asymptotic growth
+The famous prime number theorem gives information about the asymptotic growth of $\pi(n)$ as $n$ tends to
+infinity.
+\begin{thm}[Prime Number Theorem]
$$
\lim\limits_{n \rightarrow \infty}\pi(n) \sim \frac{n}{\log(n)}
$$
+\end{thm}
Given an natural number $n\geq 2$, the answer to question \eqref{eq:q1} is given by the \emph{Sieve of Erathostenes}.
The classic algorithm proceeds by starting with the set $N := \{2,\ldots,n\}$ successively erasing non-prime numbers.
Although this algorithm is not particular performant (compared to tuned versions, such as \emph{Aitken's Sieve}),
\caption{Integer-Square-Root}
\label{alg:1}
\end{algorithm}
+\begin{thm}
+ Algorithm \ref{alg:1} is correct, and terminates in a finite number of steps.
+\end{thm}
+\begin{proof}
The first step of Algorithm \ref{alg:1} is the initialization of the result $x$ and two
temporary variables $y$ and $z$. As for the While-Loop, we observe that initially
\begin{align}
y > n \Leftrightarrow (x^2+z) > n \Leftrightarrow x^2+2x+1 > n \Leftrightarrow (x+1)^2 > n,
$$
hence we have shown $x^2\leq n < (x+1)^2$, and taking square roots shows the claim.
+\end{proof}
\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}.
mathematically inclined people would already provide \emph{per se}, as a formal proof system could not use
intuition.\\
-However, we now present one possible answer to question \eqref{eq:q1}, by considering the following algorithm.
+Based on that, we now present one possible answer to question \eqref{eq:q1}, by considering the following algorithm.
\begin{algorithm}[H]
\begin{algorithmic}[1]
\Require{$n\in\mathbb{N}$ such that $n>2$}
\State $P \leftarrow \emptyset$;
\State $Q \leftarrow \{2,\ldots,n\}$;
\While{$Q \neq \emptyset$}
-\State $P\leftarrow P \cup \{\min(Q)\}$;
-\State $Q\leftarrow Q - \{m\in Q: \min(Q)|m\}$;
+\State $r \leftarrow \min(Q)$;
+\State $P\leftarrow P \cup \{r\}$;
+\State $Q\leftarrow Q - \{s\in Q: r|s\}$;
\EndWhile
\State\Return $P$.
\end{algorithmic}
\caption{Sieve of Erathostenes I}
\label{alg:2}
\end{algorithm}
-Algorithm \ref{alg:2} provides several points for discussion. First of all, both sets, $P$ and $Q$ are
-at all steps obviously subsets of $\{2,\ldots,n\}$. As this condition holds at each execution of the while
-loop, we identify this as a \emph{loop invariant}.
+Let us now discuss the steps of Algorithm \ref{alg:2}.
+We want to identify steps that hold at each execution step of the while loop,
+and are therefore \emph{loop invariants}.
+
+\subsubsection*{Identifying Loop Invariants}
+First of all, both sets, $P$ and $Q$ are subsets of $\{2,\ldots,n\}$. Therefore,
+at all stages of the algorithm, we have
+$$
+P, Q\subseteq \{2,\ldots,n\}.
+$$
+The set $P$ holds prime numbers only, as this is true initially (i.e. $P$ is the empty set and every
+element of the empty set is a prime number). For the inductive step, if $P$ holds prime numbers only and
+is extended by the least element of the set $Q$, it retains this property (in clear correspondence
+with Lemma \ref{lem:leastelemisprime}). Hence, a second invariant describing $P$ is, that every element of $P$
+is prime (and hence, the same applies for the intermediate sets $P$ obtained within this loop).\\
+
+Let us now quantify the numbers $2,\ldots,n$ in more detail. Each number $k$ is either prime or composite.
+If $k\in P$, then by the preceeding discussion $k$ is prime. Conversely, if $k\in \{2,\ldots,n\}$ is prime,
+it is never removed from the set $Q$, and therefore after finitely many steps the minimal element of $Q$ and
+therefore transferred to the set $P$. Hence, the algorithm ensures the equivalence $x\in P \Leftrightarrow x \text{ is prime}$.\\
+
+As a final observation, we remark, that every element of $P$ is smaller than any element of the set $Q$,
+as follows immediately from $a | n \Rightarrow a\leq b$ and the fact that $P$ contains only prime numbers
+and therefore proper divisors.
+
+\subsubsection*{Termination of the Algorithm}
+The termination of the algorithm is ensured by the so called \emph{termination term}.
+In the beginning, the set $Q$ is not empty, but at each execution step, elements of $Q$ are removed
+(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.
+
\subsection{The Sieve of Erathostenes II}
\begin{thebibliography}{9}
+\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.
+
+\bibitem{FuriaMeyer2}
+C. A. Furia, B. Meyer and S. Velder. \textit{Loop Invariants: Analysis, Classification, and Examples}
+ACM Computing Surveys, Vol. 46, No. 3, Article 34, January 2014.
+
\bibitem{hardylittlewood}
G.H. Hardy and E.M. Wright. \textit{An Introduction to the Theory of Numbers}.
Oxford University Press, 6. edition. 2008.
\bibitem{JML}
-\text{Java Modelling Language JML}
-\url{http://www.eecs.ucf.edu/~leavens/JML//index.shtml}
+\text{The Java Modelling Language (JML)} Home page, February
+2013 \url{http://www.jmlspecs.org}
\bibitem{Larch}
-\text{The Larch System}.
+\text{The Larch System} Home page, May 2017
\url{https://www.cs.cmu.edu/afs/cs/project/larch/www/home.html}
\bibitem{LidlNiederreiter}
projects / cfuerst / formal-numbers.git / commitdiff