examples/incremental.mlw

   1 module Ce_int32
   2
   3   use ref.Ref
   4   use export mach.int.Int32
   5
   6   meta "meta_incremental" ""
   7
   8   let dummy_update (r: ref int32)
   9     requires { to_int !r = 22}
  10     ensures {to_int !r = 42} =
  11     r := of_int 42;
  12     r := !r + !r;
  13
  14 end
  15
  16
  17 module Ce_interesting
  18
  19   use int.Int
  20   use ref.Ref
  21   use export mach.int.Int32
  22
  23   meta "meta_incremental" ""
  24
  25   let dummy_update (r: ref int32)
  26     requires { to_int !r > 22}
  27     ensures {to_int !r <= 42} =
  28     r := of_int 42;
  29     r := !r + !r;
  30
  31 end