module M

  use import ref.Ref

  use import int.Int

  function projf (l : int) : int
  =
  l+100

  meta "model_projection" function projf

  val y "model" "model_projected" "model_trace:y" :ref int

  let incr ( x "model" "model_trace:x" : ref int ): unit
  ensures { !x = old !x + 2 + !y }
  = 
  y := !y + 1;	 
  x := !x + 1;
  x := !x + 1

  let test_loop ( x "model" "model_trace:x" : ref int ): unit
  ensures { !x < old !x }
  =
  incr x;
  while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
end