diff --git a/.gitignore b/.gitignore index 575fc67333c100283ea7ee7897d0d0015cdf6c66..896d96136c981638716f846103be2a5a16c07991 100644 --- a/.gitignore +++ b/.gitignore @@ -34,6 +34,9 @@ why.conf /bench/programs/good/see/ /bench/programs/good/set/ /bench/programs/good/recfun/ +/bench/programs/good/loops/ +/bench/programs/good/po/ +/bench/valid/list/ # /bin/ /bin/why3.byte diff --git a/examples/programs/fact.mlw b/examples/programs/fact.mlw index 8ffe3faa2da32a581b7af5ff0342ddfec4e093b1..72134b929f84ea044eb1538a986d781e26d80a88 100644 --- a/examples/programs/fact.mlw +++ b/examples/programs/fact.mlw @@ -10,23 +10,41 @@ theory Fact "Factorial" end +module FactRecursive + + use import Fact + use import int.Int + + let rec fact_rec (x:int) : int variant {x} = + { x >= 0 } + if x = 0 then 1 else x * fact_rec (x-1) + { result = fact x } + +end module FactImperative -use import Fact -use import int.Int -use import module ref.Ref - -let fact_imp (x:int) : int = - { x >= 0 } - let y = ref 0 in - let r = ref 1 in - while !y < x do - invariant { 0 <= !y <= x and !r = fact !y } - y := !y + 1; - r := !r * !y - done; - !r - { result = fact x } + use import Fact + use import int.Int + use import module ref.Ref + + let fact_imp (x:int) : int = + { x >= 0 } + let y = ref 0 in + let r = ref 1 in + while !y < x do + invariant { 0 <= !y <= x and !r = fact !y } + y := !y + 1; + r := !r * !y + done; + !r + { result = fact x } end + +(* +Local Variables: +compile-command: "unset LANG; make -C ../.. examples/programs/fact.gui" +End: +*) + diff --git a/examples/programs/fact/why3session.xml b/examples/programs/fact/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..30d12001927eac536eb7fc2ce0418d1259e76c1b --- /dev/null +++ b/examples/programs/fact/why3session.xml @@ -0,0 +1,22 @@ + + + + + + + + + + + + + + + + + + + + + +