booleans.mlw 1.26 KB
Newer Older
1
module M
2

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

6
parameter incr : x:ref int -> { } unit writes x.contents { x = old x + 1 }
7

8
parameter x : ref int
9
10
11
12
13
14
15
16
17
18
19

parameter id_not_0 : x:int -> { x <> 0 } int { result = x }

parameter id : x:int -> { } int { result = x }

let test_and_1 () =
  { }
  if (incr x; !x > 0) && id !x = 1 then !x else 0+1
  { result = 1 }

let test_and_2 () =
20
  { x <> 0 }
21
22
23
24
25
26
  if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
  { result = 1 }

let test_or_1 () =
  { }
  if (incr x; !x > 0) || !x < 0 then 1 else 2
27
  { result = 1 -> x <> 0 }
28
29
30
31
32
33
34
35
36

let test_or_2 () =
  { }
  if !x = 0 || !x = 1 then !x else 1
  { 0 <= result <= 1 }

let test_not_1 () =
  { } 
  if not (!x = 0) then x := 0
37
  { x = 0 }
38
39

let test_not_2 () =
40
  { x <= 0 }
41
  while not (!x = 0) do invariant { x <= 0 } incr x done
42
  { x = 0 }
43
44
45
46

let test_all_1 () =
  { }
  (!x >= 0 && not (!x = 0) || !x >= 1)
47
  { result=True <-> x>=1 }
48
49
50
51
52

(* from Cesar Munoz's CD3D *)

  logic d : int

53
54
parameter vx : ref int
parameter vy : ref int
55
56
57
58
59
60

parameter sq : x:int -> {} int { result = x*x }

let test_cd3d () =
 { true }
 if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d  then 1 else 2
61
 { result=1 -> vx=0 and vy=0 }
62

63
end
64
65
66
67
68
69
70

(*
Local Variables: 
compile-command: "unset LANG; make -C ../../.. bench/programs/good/booleans"
End: 
*)