1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
module Example1
use ref.Ref
use int.Int
use bool.Bool
let f [@bddinfer] [@infer](x: int) : bool =
requires {x <= 0}
ensures { result = true }
let x = ref x in
let y = ref true in
while !x < 0 do
variant {0 - !x}
y := andb !y (!x < 0);
x := !x + 1
done;
!y
let f2 [@bddinfer] [@infer:oct](x: int) : bool =
requires {x <= 0}
ensures { result = true }
let x = ref x in
let y = ref true in
while !x < 0 do
variant {0 - !x}
y := andb !y (!x < 0);
x := !x + 1
done;
!y
let f3 [@bddinfer] [@infer:box](x: int) : bool =
requires {x <= 0}
ensures { result = true }
let x = ref x in
let y = ref true in
while !x < 0 do
variant {0 - !x}
y := andb !y (!x < 0);
x := !x + 1
done;
!y
end
|
