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
|
module M
use int.Int
use ref.Ref
(* side effects in tests *)
val x : ref int
val set_and_test_zero (v:int) : bool writes {x}
ensures { !x = v /\ if result=True then !x = 0 else !x <> 0 }
let p () ensures { result = 1 }
= if set_and_test_zero 0 then 1 else 2
val set_and_test_nzero (v:int) : bool writes {x}
ensures { !x = v /\ if result=True then !x <> 0 else !x = 0 }
let p2 (y:ref int)
requires { !y >= 0 }
ensures { !y = 0 }
= while set_and_test_nzero !y do
invariant { !y >= 0 } variant { !y }
y := !y - 1
done
let p3 (y:ref int)
requires { !y >= 0 }
ensures { !y = 0 }
= while let b = set_and_test_nzero !y in b do
invariant { !y >= 0 } variant { !y }
y := !y - 1
done
let p4 (y:ref int)
requires { !y >= 1 }
ensures { !y = 0 }
= while begin y := !y - 1; (set_and_test_nzero !y) end do
invariant { !y >= 1 } variant { !y }
()
done
end
|
