Commit e32fd3a7 authored by MARCHE Claude's avatar MARCHE Claude

Try Why3: missing examples files

parent 12573bfa
......@@ -273,8 +273,10 @@ pvsbin/
/src/trywhy3/trywhy3.byte
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
/src/trywhy3/ace-builds
/src/trywhy3/alt-ergo-0.99.1
/src/trywhy3/*.png
/src/trywhy3/alt-ergo-1.00-private-2015-01-29
# jessie3
/src/jessie/config.log
......
module BinaryMultiplication
use import mach.int.Int
use import ref.Ref
let mult (a b: int)
requires { b >= 0 }
ensures { result = a * b }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { 0 <= !y }
invariant { !z + !x * !y = a * b }
variant { !y }
if !y % 2 <> 0 then z := !z + !x;
x := 2 * !x;
y := !y / 2
done;
!z
end
module Test1
use BinaryMultiplication as B
let main () = B.mult 6 7
end
module Test2
use BinaryMultiplication as B
let main () = B.mult 4546729 21993833369
end
\ No newline at end of file
module Fact
use import mach.int.Int
use import int.Fact
use import ref.Ref
let fact_imp (x:int) : int
requires { x >= 0 }
ensures { result = fact x }
= let y = ref 0 in
let r = ref 1 in
while !y < x do
invariant { 0 <= !y <= x }
invariant { !r = fact !y }
variant { x - !y }
y := !y + 1;
r := !r * !y
done;
!r
let main () = (fact_imp 7, fact_imp 42)
end
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