tests/test_itp.mlw

   1
   2 module BinaryMultiplication
   3
   4   use mach.int.Int
   5   use ref.Ref
   6
   7   lemma stupid : 2+2 = 4
   8
   9   let useless (x:int) ensures { result > x }
  10   = x + 1
  11
  12   let lemma also_useless (x:int)
  13     requires { x > 0 }
  14     ensures { x + 1 >= 2 }
  15   = ()
  16
  17   let binary_mult (a b: int)
  18     requires { b >= 0 }
  19     ensures  { result = a * b }
  20   = let x = ref a in
  21     let y = ref b in
  22     let z = ref 0 in
  23     while !y <> 0 do
  24       invariant { 0 <= !y }
  25       invariant { !z + !x * !y = a * b }
  26       variant   { !y }
  27       if !y % 2 <> 0 then z := !z + !x;
  28       x := 2 * !x;
  29       y := !y / 2
  30     done;
  31     !z
  32
  33 end