new theory int.Iter

parent 126a149a
(* McCarthy's ``91'' function. *)
module McCarthy91
......@@ -18,24 +19,19 @@ module McCarthy91
(* non-recursive implementation using a while loop *)
use import module ref.Ref
use import int.Lex2
function f (x: int) : int =
if x >= 101 then x-10 else 91
(* iter_f k x = f^k(x) *)
function iter_f int int : int
axiom iter_f_0: forall x: int. iter_f 0 x = x
axiom iter_f_s: forall k x: int. 0 < k -> iter_f k x = iter_f (k-1) (f x)
function f (x: int) : int = if x >= 101 then x-10 else 91
use import int.Lex2
(* iter k x = f^k(x) *)
clone import int.Iter with type t = int, function f = f
let f91_nonrec (n0: int) =
{ }
let e = ref 1 in
let n = ref n0 in
while !e > 0 do
invariant { !e >= 0 /\ iter_f !e !n = f n0 }
invariant { !e >= 0 /\ iter !e !n = f n0 }
variant { (101 - !n + 10 * !e, !e) } with lex
if !n > 100 then begin
n := !n - 10;
......
......@@ -17,13 +17,39 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="fbd734e7f0f402db73a779f18601e0e7" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.96"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="8a179e2a9c0c5871f3ca4b30c9454518" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter f91_nonrec.1" expl="loop invariant init" sum="9d9dcf6019190aebc6117e2ad022ca91" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec.2" expl="loop invariant preservation" sum="62ae258e98f5b11457ce053d1d8bcdd4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec.3" expl="loop variant decreases" sum="983071e6f0190dc9996c9a6ee090539f" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec.4" expl="loop invariant preservation" sum="3e41e45cc79f11b87e69def8b23716d8" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.22"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec.5" expl="loop variant decreases" sum="b1410dd32953d682df07e83b9b631efa" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec.6" expl="normal postcondition" sum="13bd62c6208881320a98d3cc26ac5b18" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
......@@ -144,7 +144,6 @@ theory Power
lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m ->
power x (n * m) = power (power x n) m
end
theory NumOfParam
......@@ -227,7 +226,25 @@ theory Fact "Factorial"
end
theory Iter
use import Int
type t
function f t : t
function iter int t : t
axiom iter_0: forall x: t. iter 0 x = x
axiom iter_s: forall k: int, x: t. 0 < k -> iter k x = iter (k-1) (f x)
lemma iter_1: forall x: t. iter 1 x = f x
lemma iter_s2: forall k: int, x: t. 0 < k -> iter k x = f (iter (k-1) x)
end
theory Induction
use import Int
predicate p int
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment