class UnboundedStack { var top: Node; ghost var footprint: set; ghost var content: seq; function IsUnboundedStack(): bool reads {this} + footprint; { this in footprint && (top == null ==> content == []) && (top != null ==> top in footprint && top.footprint <= footprint && top.prev == null && content == top.content && top.Valid()) } function IsEmpty(): bool reads {this}; { content == [] } method Pop() returns (result: T) requires IsUnboundedStack() && !IsEmpty(); modifies footprint; ensures IsUnboundedStack() && content == old(content)[1..]; { result := top.val; // The following assert does the trick, because it gets inlined and thus // exposes top.next.Valid() (if top.next != null): footprint := footprint - top.footprint; top := top.next; // In a previous version of the implementation of the SplitExpr transformation, the // following assert did not have the intended effect of being used as a lemma: assert top != null ==> top.Valid(); if (top != null) { footprint := footprint + top.footprint; top.prev := null; } content := content[1..]; } } class Node { var val: T; var next: Node; var prev: Node; var footprint: set>; var content: seq; function Valid(): bool reads this, footprint; { this in footprint && !(null in footprint) && (next == null ==> content == [val]) && (next != null ==> next in footprint && next.footprint < footprint && !(this in next.footprint) && next.prev == this && content == [val] + next.content && next.Valid()) } } // --------------------------------------------------------------------------------------- // The following examples requires that quantifiers are boosted (that is, #2) when checked // versus not boosted (#1) when assumed. function F(x: nat): int { if x == 0 then 0 else 1 + F(x-1) } method M(N: nat) { var i := 0; while (i < N) invariant forall x {:induction false} :: 0 <= x <= i ==> F(x) == x; { i := i + 1; } } // ----- orderings of checked vs. free ----- // The translation must always put checked things before free things. In most situations, // this does not actually matter, but it does matter for loop invariants of loops that have // no backedges (that is, loops where Boogie's simple dead-code analysis figures prunes // away the backedges. predicate AnyPredicate(a: int, b: int) { a <= b } method NoLoop(N: nat) { var i; while i < N invariant AnyPredicate(i, N); // error: may not hold initially { i := i + 1; break; // this makes the loop not a loop } assert AnyPredicate(i, N); }