class UnboundedStack { var top: Node; ghost var content: seq; function IsUnboundedStack(): bool reads this, this.top, this.top.footprint; { (top == null ==> content == []) && (top != null ==> content == top.content && top.Valid()) } method InitUnboundedStack() modifies this; ensures IsUnboundedStack(); ensures content == []; { this.top := null; this.content := []; } method Push(val: Object) requires IsUnboundedStack(); modifies this; ensures IsUnboundedStack(); ensures content == [val] + old(content); { var tmp := new Node; call tmp.InitNode(val,top); top := tmp; content := [val] + content; } method Pop() returns (result: Object) requires IsUnboundedStack(); requires content != []; modifies this; ensures IsUnboundedStack(); ensures content == old(content)[1..]; { result := top.val; top := top.next; content := content[1..]; } method isEmpty() returns (result: bool) requires IsUnboundedStack(); ensures result == (content == []); { result := (top == null); } /* method incorrect(n: Node) requires IsUnboundedStack(); requires n != null && n != top; modifies n; ensures IsUnboundedStack(); { n.next := top; } */ }