Readability, no functional changes

diff --git a/discrete_log.txt b/discrete_log.txt
index e92aa12..2db452e 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -9,9 +9,7 @@ type prime = ℕ[K];
 type res = ℕ[L];
 
 pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n;
-
 pred isPrime(m:prime) ⇔ ∀n:prime. divides(n,m) ⇒ (n ≤ 1 ∨ n = m);
-
 pred isComposite(m:prime) ⇔ ¬isPrime(m);
 
 proc InvModP(a:ℕ[K^2],p:prime): prime
@@ -26,7 +24,6 @@ proc InvModP(a:ℕ[K^2],p:prime): prime
      decreases p-i;
      if a*i % p = 1 then    // straight search
         ainv = i;           // algorithmic alternative: Euclidean algorithm   
-
    return ainv;
 }
 
@@ -44,7 +41,6 @@ proc IntegerRoot(a:nat): nat
       z=z+2;
       y=y+z;
    }
-
    return x;
 }
 
@@ -63,8 +59,7 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
    var gi:prime = InvModP(g,p);
    var solFound:Bool := false;
   
-   A[0] := 1;
-   b[0] := a;
+   A[0] := 1;  b[0] := a;
  
    for var i:nat=1;i<=m;i=i+1 do
       decreases m+1-i;
@@ -81,14 +76,12 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
       {
          if A[j] = b[i] then
          {
-            // result found
             ret = i*m + j;
             solFound = true;
          }
       }
       b[i+1] = b[i]*gim % p; // Giant-Step
    }   
-
    return ret;
 }
 

diff --git a/report/formal.pdf b/report/formal.pdf
index 600a46b..a7d5b0a 100644 (file)
Binary files a/report/formal.pdf and b/report/formal.pdf differ

diff --git a/report/formal.tex b/report/formal.tex
index 4bea1c0..4c0cc8c 100644 (file)
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -253,7 +253,7 @@ The algorithm proceeds by first compiling a table with entries $(i,t_i)$ where $
 (computed by repeated multiplying modulo $p$).
 The table consists of $m := \lceil \sqrt{p-1}\,\rceil$ entries from 0 to $m-1$.
 In the next step, one computes $g^{-m}\pmod p$. Initialize an index $i$ with zero.
-If $a_i$ happens to coincide with some $t_j$ where $0\leq j\leq m-1$, then the 
+If $a_i$ happens to coincide with some $t_j$ where $0\leq j\leq m-1$, then the
 algorithm terminates with $x=i\cdot m + j$, otherwise it computes $a_{i+1} = a_i g^{-m}\pmod p$.
 An implementation of this algorithm in \CC\, might be written as follows:
 {\tiny \lstinputlisting{../src/discrete_log.cpp}}
@@ -440,7 +440,7 @@ Some comments on the formalization:
  \item The first argument is the characteristic of the finite field, which is a prime.
        Below 10, the primes are 2,3,5,7. Obviously, for $p=2$ we have no elements of
        order $p-1$;
- \item The condition that $g$ has to be of order $p-1$ is a major restriction. 
+ \item The condition that $g$ has to be of order $p-1$ is a major restriction.
  The only elements that satisfy this are given by
 \end{itemize}
 \begin{center}
@@ -451,8 +451,8 @@ $p$ & Elements of order $p-1$\\
 3  & 2 \\
 5  & 2,3\\
 7  & 3,5\\
-\hline 
-\end{tabular} 
+\hline
+\end{tabular}
 \end{center}
 \begin{itemize}
  \item The element $a$ has obviously to be non-zero in $\mathbb{Z}_p$.
@@ -465,13 +465,33 @@ are in our scope might be explictly enumerated by
 $(p,g,a)$\\
 \hline
 $(3,2,1)$, $(3,2,2)$\\
-$(5,2,1)$,$(5,2,2)$,$(5,2,3)$,$(5,2,4)$\\ 
+$(5,2,1)$,$(5,2,2)$,$(5,2,3)$,$(5,2,4)$\\
 $(5,3,1)$,  $(5,3,2)$,  $(5,3,3)$, $(5,3,4)$\\
  $(7,3,1)$, $(7,3,2)$, $(7,3,3)$,  $(7,3,4)$, $(7,3,5)$, $(7,3,6)$ \\
-$(7,5,1)$,  $(7,5,2)$,  $(7,5,3)$, $(7,5,4)$,  $(7,5,5)$, $(7,5,6)$ 
-\end{tabular} 
+$(7,5,1)$,  $(7,5,2)$,  $(7,5,3)$, $(7,5,4)$,  $(7,5,5)$, $(7,5,6)$
+\end{tabular}
 \end{center}
 which gives a total of 22 elements to check.
+
+\subsection{Prime Number Generation}
+A classic algorithm for generating prime-numbers less equal a given number, is the Sieve of Erathostenes.
+Suppose, we want to produce a list of all primes less equal $m$, the algorithm proceeds by enumerating
+all integers from 2 to $m$, we set $S^{(0)}:=\{2,\ldots,m\}$. The first prime, is obviously given by 2, i.e.
+the minimal element of the set $S^{(0)}$. Of course, any number greater and divisible by 2 is not prime,
+hence, we remove the \emph{even} elements from the set $S^{(0)}$ to obtain the set $S^{(1)}$. The next prime
+number is the least number of the updated set $S^{(1)}$, i.e. 3. We remove all multiples of 3 to obtain
+$S^{(2)}$. Proceedings likewise, up to $\sqrt{m}$, by selecting the minimal element $p$ (which is prime)
+of $S^{(k)}$ and updating $S^{(k)}$ to $S^{(k+1)}$, that is, removing all multiples of $p$, we obtain a list
+of primes less equal $m$.\\
+
+We formalize this algorithm in two ways. While the first formalization treats the numbers 2..$m$ as boolean
+array, we can for the second formalization the data structure of sets (that corresponds to sets in the
+mathematical sense). Obviously, we should obtain the same results.
+
+\subsection*{The RISCAL Formalization}
+{\scriptsize \verbatimboxed{../sieveEratosthenes.txt}}
+
+
 \appendix
 
 

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index 0ae53d4..11a16ce 100644 (file)
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -6,7 +6,6 @@ pred divides(m:nat,n:nat) ⇔ ∃p:nat. m⋅p = n;
 pred isPrime(m:nat) ⇔ (m = 0) ∨ (m=1) ∨
                       (1 < m ∧ ∀n:nat. divides(n,m) ⇒ (n≤1 ∨ n=m));
 
-
 proc IntegerRoot(a:nat): nat
    ensures result^2 ≤ a ∧ a < (result+1)^2;
 {
@@ -21,7 +20,6 @@ proc IntegerRoot(a:nat): nat
       z=z+2;
       y=y+z;
    }
-
    return x;
 }
 
@@ -38,14 +36,14 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
    for i=2; i≤IntegerRoot(m); i=i+1 do
       decreases IntegerRoot(m)+1-i;
    {
-         if ret[i] = true then
-         {
-            for k=0;i^2+k*i<MAX;k=k+1 do
-            {
-            j=i^2+k*i;
-               ret[j] = false;
-            }
-         }
+        if ret[i] = true then
+        {
+            for k=0;i^2+k*i<MAX;k=k+1 do
+            {
+                j=i^2+k*i;
+                ret[j] = false;
+            }
+        }
    }
    return ret;
 }
@@ -57,9 +55,12 @@ proc SetMin(s:Set[ℕ[MAX]]): ℕ[MAX]
    var ret:ℕ[MAX] := MAX;
 
    for x in s do
+   {
      if x < ret then
+     {
         ret = x;
-
+     }        
+   }
    return ret;
 }
 
@@ -75,10 +76,9 @@ proc SieveOfErathostenesSet(m:ℕ[MAX]): Set[ℕ[MAX]]
       invariant ∀e ∈ ret. isPrime(e);
    {
       locmi = SetMin(start);
-         ret = ret ∪ {locmi};
-         start = start \ ({locmi} ∪ { if divides(locmi,x) then x else locmi | x ∈ start});
+      ret = ret ∪ {locmi};
+      start = start \ ({locmi} ∪ { if divides(locmi,x) then x else locmi | x ∈ start});
    }
    return ret;
 }
 
-