tests-uint32.mlw 508 Bytes
Newer Older
1 2 3

module TestInt32

4
  use mach_int.Int32
5 6 7 8 9 10 11 12 13 14 15 16 17

  let mean_wrong (a:int32) (b:int32) : int32 =
    div (add a b) (of_int 2)

  let mean_ok (a:int32) (b:int32) : int32 
    requires { 0 <= to_int a <= to_int b }
  =
    add a (div (sub b a) (of_int 2))

end   

module TestUInt32

18
  use mach_int.UInt32
19 20 21 22 23 24 25 26 27 28

  let mean_wrong (a:uint32) (b:uint32) : uint32 =
    div (add a b) (of_int 2)

  let mean_ok (a:uint32) (b:uint32) : uint32 
    requires { to_int a <= to_int b }
  =
    add a (div (sub b a) (of_int 2))

end