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

2
3
4
5
6
let foo () = 
  {}
  any {} int {result=2}  + 1
  {result=3}

7
8
9
10
11
12
13
14
let rec div x y variant {x} =
  { 0 <= x and 0 < y }
  if y < x then 
    (0, x)
  else 
    let (q,r) = div (x-y) y in (q+1, r)
  { let (q,r) = result in x = q*y + r and 0 <= r < x }

15
{ 
16
  type tree 'a = 
17
18
     | Empty
     | Node (tree 'a) 'a (tree 'a)
19
}
20
21
22
23
let rec mem x t = match t : tree int with
  | Empty -> False
  | Node l y r -> x=y || mem x (if x < y then l else r)
  end
24

25
26
let root t : 'a = 
  { t <> Empty }
27
  match t with
28
29
  | Empty -> absurd
  | Node _ x _ -> x
30
  end
31
  { }
32

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