Turing's proof variant with 'for' loops

parent c9f1acd0
......@@ -9,6 +9,7 @@ module CheckingALargeRoutine
use import int.Fact
use import module ref.Ref
(* using 'while' loops, to keep close to Turing's flowchart *)
let routine (n: int) =
{ n >= 0 }
let r = ref 0 in
......@@ -29,6 +30,19 @@ module CheckingALargeRoutine
!u
{ result = fact n }
(* using 'for' loops, for clearer code and annotations *)
let routine2 (n: int) =
{ n >= 0 }
let u = ref 1 in
for r = 0 to n-1 do invariant { !u = fact r }
let v = !u in
for s = 1 to r do invariant { !u = s * fact r }
u := !u + v
done
done;
!u
{ result = fact n }
end
(*
......
......@@ -42,6 +42,30 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter routine2" expl="correctness of parameter routine2" sum="32b32b9b9b318e64648a8ba9f7e5d5f1" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter routine2.1" expl="normal postcondition" sum="75e62e35864ac471be567cac42bc187d" 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 routine2.2" expl="for loop initialization" sum="816bea4bc7d46893fc6b81e308cd8a15" 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 routine2.3" expl="for loop preservation" sum="e329eb985039879c3ec9ef5f8a2b26bb" 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 routine2.4" expl="normal postcondition" sum="b9db04f424b86930562c0dcb84eba2a8" 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>
</why3session>
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