Update after second Review Wolfgang

diff --git a/discrete_log.txt b/discrete_log.txt
index 13ad706..3193ae5 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -43,6 +43,7 @@ proc IntegerRoot(a:nat): nat
 
    while y ≤ a do
       invariant x^2 ≤ a ∧ y = x^2+z ∧ z = 2*x+1;
+      decreases a-x^2;
    {
       x=x+1;
       z=z+2;
@@ -98,3 +99,4 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
 
 
 
+

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index 6b27a8a..a26805b 100644 (file)
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -14,6 +14,7 @@ proc IntegerRoot(a:nat): nat
 
    while y ≤ a do
       invariant x^2 ≤ a ∧ y = x^2+z ∧ z = 2*x+1;
+      decreases a-x^2;
    {
       x=x+1;
       z=z+2;
@@ -48,11 +49,13 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
 
 proc SetMin(s:Set[nat]): nat
    requires s ≠ ∅[nat];
+   requires ∀e ∈ s. e ≤ MAX;
    ensures result ∈ s ∧ ∀e ∈ s. result ≤ e;
 {
    var ret:nat := MAX;
 
    for x in s do
+      invariant ∀e in forSet. ret ≤ e;
    {
      if x < ret then
      {
@@ -67,6 +70,8 @@ fun SetMin2(s:Set[nat]): nat
     ensures result ∈ s ∧ ∀e ∈ s. result ≤ e;
  = choose m in s with ∀e in s. m <= e;
 
+theorem PrimeDivisor() ⇔ ∀e:nat. (e > 1 ∧ ¬isPrime(e)) ⇒ ∃p:nat. p<e ∧ isPrime(p) ∧ e%p = 0;
+
 proc SieveOfErathostenesSet(m:nat): Set[nat]
    ensures ∀e:nat. e ≤ m ⇒ (e ∈ result ⇔ isPrime(e));
 {
@@ -74,7 +79,11 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
    var ret:Set[nat]   := ∅[nat]; 
 
    while start ≠ ∅[nat] do
-      invariant ret ⊆ 2..m ∧ ∀e ∈ ret. isPrime(e);
+      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 ⇒ ¬ (e ∈ ret);
    {
       var locmi:nat = SetMin(start);
       ret = ret ∪ {locmi};
@@ -84,3 +93,5 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
 }
 
 
+
+