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
|
module Unreachable
use int.Int
use ref.Ref
use mach.java.lang.Integer
let return1972 () : integer
ensures { result = 1972 }
=
let i : ref integer = ref 0 in
while true do
invariant { !i <= 1972 }
variant { 1972 - !i }
if !i = (1972:integer) then
return !i;
i := !i+1;
done;
absurd
end
module UnreachableFixed
use int.Int
use ref.Ref
use mach.java.lang.Integer
let return1972 () : integer
ensures { result = 1972 }
=
let i : ref integer = ref 0 in
let j : ref integer = ref 1 in
while !j > 0 do
invariant { !i <= 1972 }
variant { 1972 - !i }
if !i = (1972:integer) then
return !i;
i := !i+1;
done;
absurd
end
|
