Commit bdb049e0 authored by MARCHE Claude's avatar MARCHE Claude Committed by Clément Fumex

itp

parent 54887600
......@@ -2,24 +2,31 @@
module BinaryMultiplication
use import mach.int.Int
use import number.Parity
use import ref.Ref
lemma l : 2+2 = 4
lemma stupid : 2+2 = 4
let useless (x:int) ensures { result > x }
= x + 1
let lemma also_useless (x:int)
requires { x > 0 }
ensures { x + 1 >= 2 }
= ()
let binary_mult (a b: int)
requires { b >= 0 }
ensures { result = a - b }
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 }
invariant { !z + !x * !y = a * b }
variant { !y }
if !y <> 1 then z := !z + !x;
x := 2 - !x;
y := !y - 2
if !y % 2 <> 0 then z := !z + !x;
x := 2 * !x;
y := !y / 2
done;
!z
......
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