Skip to content

GitLab

why3
why3
Commit c9f1acd0 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

moved Fact to library int, split fact.mlw into two files

parent 57af3d95
Hide whitespace changes
Inline Side-by-side
Showing with 113 additions and 66 deletions
examples/programs/checking_a_large_routine.mlw 0 → 100644
View file @ c9f1acd0
(* 'Checking a large routine' Alan Mathison Turing, 1949
One of the earliest proof of program.
The routine computes n! using only additions, with two nested loops.
*)
module CheckingALargeRoutine
use import int.Fact
use import module ref.Ref
let routine (n: int) =
{ n >= 0 }
let r = ref 0 in
let u = ref 1 in
while !r < n do
invariant { 0 <= !r <= n /\ !u = fact !r }
variant { n - !r }
let s = ref 1 in
let v = !u in
while !s <= !r do
invariant { 1 <= !s <= !r + 1 /\ !u = !s * fact !r }
variant { !r - !s }
u := !u + v;
s := !s + 1
done;
r := !r + 1
done;
!u
{ result = fact n }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/checking_a_large_routine.gui"
End:
*)
examples/programs/checking_a_large_routine/why3session.xml 0 → 100644
View file @ c9f1acd0
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/checking_a_large_routine/why3session.xml">
<file name="../checking_a_large_routine.mlw" verified="true" expanded="true">
<theory name="WP CheckingALargeRoutine" verified="true" expanded="true">
<goal name="WP_parameter routine" expl="correctness of parameter routine" sum="1a0cf6427e5788cffb6e08acc3d9f854" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter routine.1" expl="loop invariant init" sum="64c778b45784b39624f6b7d0ec35426f" 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 routine.2" expl="loop invariant init" sum="b1e34b8f90b5b768f13899eea71250b3" 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 routine.3" expl="loop invariant preservation" sum="8b92371d31cbb9f54824b7e5ebc0d711" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter routine.4" expl="loop variant decreases" sum="d90372dd9d9ac09e304c5b72ae826f54" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter routine.5" expl="loop invariant preservation" sum="85ac06138a1caf9b62fe9f27784d8207" 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 routine.6" expl="loop variant decreases" sum="793aca3c87d07879b23edad05db3a677" 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 routine.7" expl="normal postcondition" sum="b5595a595985a84708bb85f6e9cc9749" 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>
examples/programs/fact.mlw
View file @ c9f1acd0
(* Various programs computing the factorial. *)
theory Fact "Factorial"
use export int.Int
function fact int : int
axiom fact0: fact 0 = 1
axiom factn: forall n:int. n >= 1 -> fact n = fact (n-1) * n
end
module FactRecursive
use import Fact
use import int.Int
use import int.Fact
let rec fact_rec (x:int) : int variant {x} =
{ x >= 0 }
......@@ -26,8 +14,7 @@ end
module FactImperative
use import Fact
use import int.Int
use import int.Fact
use import module ref.Ref
let fact_imp (x:int) : int =
......@@ -44,41 +31,6 @@ module FactImperative
end
(* 'Checking a large routine' Alan Mathison Turing, 1949
One of the earliest proof of program.
The routine computes n! using only additions, with two nested loops.
*)
module CheckingALargeRoutine
use import Fact
use import int.Int
use import module ref.Ref
let routine (n: int) =
{ n >= 0 }
let r = ref 0 in
let u = ref 1 in
while !r < n do
invariant { 0 <= !r <= n /\ !u = fact !r }
variant { n - !r }
let s = ref 1 in
let v = !u in
while !s <= !r do
invariant { 1 <= !s <= !r + 1 /\ !u = !s * fact !r }
variant { !r - !s }
u := !u + v;
s := !s + 1
done;
r := !r + 1
done;
!u
{ result = fact n }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/fact.gui"
......
examples/programs/fact/why3session.xml
View file @ c9f1acd0
......@@ -2,56 +2,54 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/fact/why3session.xml">
<file name="../fact.mlw" verified="true" expanded="true">
<theory name="Fact" verified="true" expanded="true">
</theory>
<theory name="WP FactRecursive" verified="true" expanded="true">
<goal name="WP_parameter fact_rec" expl="correctness of parameter fact_rec" sum="1bff2d72d2a37c866be6a82c2fda007e" proved="true" expanded="true">
<goal name="WP_parameter fact_rec" expl="correctness of parameter fact_rec" sum="9f6baede150e73fa6e0ed1159fe37404" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory name="WP FactImperative" verified="true" expanded="true">
<goal name="WP_parameter fact_imp" expl="correctness of parameter fact_imp" sum="5a3dec0b98b32ea14e04a5cdc91a245c" proved="true" expanded="true">
<goal name="WP_parameter fact_imp" expl="correctness of parameter fact_imp" sum="e31ce81a222a20fd268e4969688b6dfb" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory name="WP CheckingALargeRoutine" verified="true" expanded="true">
<goal name="WP_parameter routine" expl="correctness of parameter routine" sum="037dcf30692294fab4727f024ea94e46" proved="true" expanded="true">
<goal name="WP_parameter routine" expl="correctness of parameter routine" sum="1a0cf6427e5788cffb6e08acc3d9f854" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter routine.1" expl="loop invariant init" sum="9a5b92f18bf024980c5dd8bdcfdfba50" proved="true" expanded="true">
<goal name="WP_parameter routine.1" expl="loop invariant init" sum="64c778b45784b39624f6b7d0ec35426f" 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 routine.2" expl="loop invariant init" sum="1a76deb02167a0eebac08097f4ce6236" proved="true" expanded="true">
<goal name="WP_parameter routine.2" expl="loop invariant init" sum="b1e34b8f90b5b768f13899eea71250b3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.3" expl="loop invariant preservation" sum="28796e0502fc673a5466eb318ef0d40a" proved="true" expanded="true">
<goal name="WP_parameter routine.3" expl="loop invariant preservation" sum="8b92371d31cbb9f54824b7e5ebc0d711" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter routine.4" expl="loop variant decreases" sum="97cfc3343b8c5a9b18f67172c73d9498" proved="true" expanded="true">
<goal name="WP_parameter routine.4" expl="loop variant decreases" sum="d90372dd9d9ac09e304c5b72ae826f54" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.5" expl="loop invariant preservation" sum="11e0ddb1cbd4de5dc5ebf78b1a6b9f17" proved="true" expanded="true">
<goal name="WP_parameter routine.5" expl="loop invariant preservation" sum="85ac06138a1caf9b62fe9f27784d8207" 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 routine.6" expl="loop variant decreases" sum="cbef992a4fc1e57d0560fddcf4f18ed2" proved="true" expanded="true">
<goal name="WP_parameter routine.6" expl="loop variant decreases" sum="793aca3c87d07879b23edad05db3a677" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.7" expl="normal postcondition" sum="f4ab075ae1ee0bb8205be10749ecdc78" proved="true" expanded="true">
<goal name="WP_parameter routine.7" expl="normal postcondition" sum="b5595a595985a84708bb85f6e9cc9749" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......
theories/int.why
View file @ c9f1acd0
......@@ -216,6 +216,17 @@ theory NumOf
end
theory Fact "Factorial"
use export Int
function fact int : int
axiom fact0: fact 0 = 1
axiom factn: forall n:int. n >= 1 -> fact n = n * fact (n-1)
end
(* number theory *)
theory Divisibility
......
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