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

2 3
module P

4
  use import int.Int
5
  use import module stdlib.Ref
6

7 8 9 10 11 12 13 14 15 16 17
  use import list.List
  use import list.Length

let rec length_ (l : list 'a) variant { length l } = 
  {}
  match l with
  | Nil -> 0
  | Cons _ r -> 1 + length_ r
  end
  { result = length l }

18
  (* parameter b : ref int *)
19

20 21
  (* let f () =  *)
  (*   { b>0 } !b + 1 { result > b } *)
22

23 24 25 26 27 28
  let test r =
    { r = 1 }
    assert { r = 1 };
    r := !r + 1;
    assert { r = 2 }
    { true }
29

30
end
31

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