blob: f7a44cfea5aa72a85dcef1a5b3a4e24603819f49 (
plain)
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
// This test case showed a triggering problem (and potentially a matching loop).
// The quantified assertion and postcondition that did not verify are highlighted below.
class Node
{
var val:int
var next:Node
var break_here:bool
predicate lseg
{
acc(break_here) && (!break_here ==> acc(val) && acc(next) && (next!=null ==> next.lseg))
}
predicate xlseg
{
acc(val) && acc(next) && (next!=null ==> next.lseg)
}
function length():int
requires lseg
ensures 0 <= result
{
unfolding lseg in (break_here ? 0 : (next==null ? 1 : 1+next.length()))
}
function xlength():int
requires xlseg
ensures 0 < result
{
unfolding xlseg in (next==null ? 1 : 1+next.length())
}
function get(i:int):int
requires lseg && i>=0 && i<length()
{
unfolding lseg in i==0 ? val : next.get(i-1)
}
function xget(i:int):int
requires xlseg && i>=0 && i<xlength()
{
unfolding xlseg in i==0 ? val : next.get(i-1)
}
function get_next_seg():Node
requires lseg
{
unfolding lseg in break_here ? this : (next==null ? next : next.get_next_seg())
}
method lastNode() returns(res:Node)
requires lseg && length()>0
ensures res != null && lseg && res.xlseg
ensures res.xlength()==1 && res.xget(0)==old(get(length()-1))
ensures length() == old(length()-1)
// Did not verify.
ensures (forall i:int :: 0<=i && i<length() ==> get(i) == old(get(i)))
{
var I:int
var h:Node
res:=this
unfold lseg
break_here:=true
fold lseg
fold xlseg
while(res.xlength()>1)
invariant res!=null && lseg && res.xlseg &&
res==get_next_seg() && // new invariant
length() + res.xlength() == old(length()) &&
0 <= length() && length() < old(length()) &&
(forall i:int :: 0<=i && i<length() ==> get(i)==old(get(i))) &&
(forall i:int :: length()<=i && i<old(length()) ==> res.xget(i-length())==old(get(i)))
{
// We are not interested (at the moment) in verifying the loop.
assume false
}
// Did not verify.
assert (forall i:int :: length()<=i && i<old(length()) ==> res.xget(i-length())==old(get(i)))
}
}
|
