test.mlw 539 Bytes
Newer Older
1 2 3

(* test file for ML-why *)

4 5 6 7 8 9
{ 
use import prelude.Int
logic f(int) : int 
logic g(x : int) : int = f(x+1)
}

10
let p = 
11 12 13 14 15 16 17 18 19
  if !x = 1 then begin end else ghost begin !x end;
  L:
  assert { !x = 0 };
  check { false };
  let z = !x + !x in
  let t = ghost (ref 2) in
  assume { true -> old(!z) = 2 }; 
  while !x >= 0 do
    invariant { true } variant { t }
20
    x := 2
21
  done;
22
  (* for x in s do () done; *)
23
  f !x
24

25 26 27
{ 
axiom A : forall x:int. f(x) = g(x-1)
}
28

29

30 31 32 33 34
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)