tests/tests-uint32.mlw

   1
   2 module TestInt32
   3
   4   use mach_int.Int32
   5
   6   let mean_wrong (a:int32) (b:int32) : int32 =
   7     div (add a b) (of_int 2)
   8
   9   let mean_ok (a:int32) (b:int32) : int32
  10     requires { 0 <= to_int a <= to_int b }
  11   =
  12     add a (div (sub b a) (of_int 2))
  13
  14 end
  15
  16 module TestUInt32
  17
  18   use mach_int.UInt32
  19
  20   let mean_wrong (a:uint32) (b:uint32) : uint32 =
  21     div (add a b) (of_int 2)
  22
  23   let mean_ok (a:uint32) (b:uint32) : uint32
  24     requires { to_int a <= to_int b }
  25   =
  26     add a (div (sub b a) (of_int 2))
  27
  28 end