factorial example updated and added to the nightly bench

parent fe8cd6a9
...@@ -34,6 +34,9 @@ why.conf ...@@ -34,6 +34,9 @@ why.conf
/bench/programs/good/see/ /bench/programs/good/see/
/bench/programs/good/set/ /bench/programs/good/set/
/bench/programs/good/recfun/ /bench/programs/good/recfun/
/bench/programs/good/loops/
/bench/programs/good/po/
/bench/valid/list/
# /bin/ # /bin/
/bin/why3.byte /bin/why3.byte
......
...@@ -10,23 +10,41 @@ theory Fact "Factorial" ...@@ -10,23 +10,41 @@ theory Fact "Factorial"
end 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 module FactImperative
use import Fact use import Fact
use import int.Int use import int.Int
use import module ref.Ref use import module ref.Ref
let fact_imp (x:int) : int = let fact_imp (x:int) : int =
{ x >= 0 } { x >= 0 }
let y = ref 0 in let y = ref 0 in
let r = ref 1 in let r = ref 1 in
while !y < x do while !y < x do
invariant { 0 <= !y <= x and !r = fact !y } invariant { 0 <= !y <= x and !r = fact !y }
y := !y + 1; y := !y + 1;
r := !r * !y r := !r * !y
done; done;
!r !r
{ result = fact x } { result = fact x }
end end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/fact.gui"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!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="FactRecursive" verified="true" expanded="true">
<goal name="WP_parameter fact_rec" expl="correctness of parameter fact_rec" sum="26ddbd98b20d38d8cc8174af1ddddb03" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory name="FactImperative" verified="true" expanded="true">
<goal name="WP_parameter fact_imp" expl="correctness of parameter fact_imp" sum="e351701b7425629858770982d2abae90" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</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