Commit 24626f5d by Jean-Christophe Filliâtre

fixed example program power

parent 30f16670
 ... @@ -23,7 +23,7 @@ module M ... @@ -23,7 +23,7 @@ module M let p = ref x in let p = ref x in let e = ref n in let e = ref n in while !e > 0 do while !e > 0 do invariant { r * power x e = power x n } invariant { 0 <= e and r * power p e = power x n } variant { e } variant { e } if mod !e 2 = 1 then r := !r * !p; if mod !e 2 = 1 then r := !r * !p; p := !p * !p; p := !p * !p; ... ...
 ... @@ -102,12 +102,15 @@ theory Power ... @@ -102,12 +102,15 @@ theory Power axiom Power_s : forall x n : int. 0 < n -> power x n = x * power x (n-1) axiom Power_s : forall x n : int. 0 < n -> power x n = x * power x (n-1) lemma Power_1 : forall x : int. power x 1 = x lemma Power_sum : forall x n m : int. 0 <= n -> 0 <= m -> lemma Power_sum : forall x n m : int. 0 <= n -> 0 <= m -> power x (n + m) = power x n * power x m power x (n + m) = power x n * power x m lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m -> lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m -> power x (n * m) = power (power x n) m power x (n * m) = power (power x n) m end end theory NumOfParam theory NumOfParam ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!