test-pgm-jcf.mlw 1.04 KB
Newer Older
1

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

7 8 9 10 11
exception Not_found
exception Found of int

let test_raise (x:bool) = raise Not_found : int 

12 13
let test (n:int) = 
  let rec is_even (x:int) = 
14 15
    {true} 
    is_even x : int
16 17 18
    {true}
  in
  is_even n
19

20
let rec is_even (x:int) variant {x} = 
21 22 23 24
    {x>=1} 
    if x = 0 then True else not (is_odd (x-1))
    {true}

25
and is_odd (x:int) variant {x} =
26 27 28 29
  if x = 0 then False else not (is_even (x-1))

let b = is_even 2

30 31 32 33 34 35 36
let rec mem (x:int) (l:int list) = 
  { true }
  match l with
  | Nil -> True
  | Cons (y, r) -> x = y || mem x r
  end
  { true }
37

38
let p =
39
  let x = ref 0 in
40 41
  x := 1;
  assert { !x = 1 };
42
  label L:
43
  assume { at(!x, L) = 2 };
44
  absurd : int ref
45

46 47 48 49
let f (x : int ref) = 
  { !x >= 0 }
  (fun y -> { y >= 0 } y+1 { result > y }) 2
  { result > 0 and old(!x)>=0 }
50

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

53 54 55
parameter r : int ref

let foo = g 2 r
56

57 58 59 60 61
let p12 () =
  let x = any int in
  x + any int
  

62 63
(*
Local Variables: 
64
compile-command: "unset LANG; make -C .. testl"
65 66
End: 
*)