Chalice/tests/predicates/test10.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

class List
{
  var value:int;
  var next:List;
  
  predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }
  
  function get():int
    requires inv;
  { unfolding inv in value }
  
  method foo()
    requires inv && unfolding inv in next!=null;
	ensures inv && unfolding inv in next!=null;
  {
    assert unfolding inv in unfolding next.inv in true;
  }
}