test-pgm-jcf.mlw 576 Bytes
Newer Older
1

2
3
{ 
use import list.List
4
logic c : int
5
6
}

7
8
let p = c

9
(*
10
11
12
13
14
15
16
let rec mem (x:int) (l:int list) = 
  { true }
  match l with
  | Nil -> True
  | Cons (y, r) -> x = y || mem x r
  end
  { true }
17
*)
18

19
let p =
20
  let x = ref 0 in
21
22
  x := 1;
  assert { !x = 1 };
23
  label L:
24
  assume { at(!x, L) = 2 };
25
  absurd : int ref
26

27
28
29
30
let f (x : int ref) = 
  { !x >= 0 }
  (fun y -> { y >= 0 } y+1 { result > y }) 2
  { result > 0 and old(!x)>=0 }
31

32
33
parameter g : x:int -> y:int ref -> { true } int { result = x + old(!y) }

34
35
(*
Local Variables: 
36
compile-command: "unset LANG; make -C .. testl"
37
38
End: 
*)