Chalice/tests/predicates/framing-functions.chalice


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

class List
{
  var value:int;
  var next:List;
  predicate valid { acc(value) && acc(next) && (next!=null ==> next.valid) }
 
  method set(x:int, y:int) requires valid; ensures valid; {}
  
  function itemAt(i: int): int
    requires valid && 0 <= i;
  { unfolding valid in i == 0 || next == null ? value : next.itemAt(i-1) }
}

class C
{
  method M (x:List, y:List)
    requires x!=null && y!=null && x!=y && x.valid && y.valid;
  {
    var i: int := x.itemAt(0);
	var j: int := y.itemAt(0);
    call y.set(0,10);
    assert i==x.itemAt(0); // succeeds
    assert j==y.itemAt(0); // correctly fails to verify
 }
}