bench/check-ce/model_projection.mlw

   1
   2 use int.Int
   3
   4 type t
   5
   6 function to_map t : int -> int
   7 meta "model_projection" function to_map
   8
   9 function get t int : int
  10 val get (m:t) (x:int) : int
  11   ensures { result = get m x }
  12
  13 function set t int int : t
  14 val set (m:t) (x:int) (y:int) : t
  15   ensures { result = set m x y }
  16
  17 type s = { mutable d : t }
  18
  19 val y : s
  20
  21 let g1 () : unit =
  22   y.d <- set y.d 1 2 ;
  23   assert { get y.d 13 < 41 \/ to_map y.d 14 < 42 }