class UnboundedStack { ghost var representation: set; ghost var content: seq; var top: Node; function IsUnboundedStack(): bool reads this, representation; { this in representation && (top == null ==> content == []) && (top != null ==> top in representation && this !in top.footprint && top.footprint <= representation && content == top.content && top.Valid()) } method InitUnboundedStack() modifies this; ensures IsUnboundedStack(); ensures content == []; { this.top := null; this.content := []; this.representation := {this}; } method Push(val: T) requires IsUnboundedStack(); modifies this; ensures IsUnboundedStack(); ensures content == [val] + old(content); { var tmp := new Node; call tmp.InitNode(val,top); top := tmp; representation := representation + top.footprint; content := [val] + content; } method Pop() returns (result: T) 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; } } class Node { ghost var footprint: set; ghost var content: seq; var val: T; var next: Node; function Valid(): bool reads this, footprint; { this in footprint && (next == null ==> content == [val]) && (next != null ==> next in footprint && next.footprint <= footprint && this !in next.footprint && content == [val] + next.content && next.Valid()) } method InitNode(val: T, next: Node) requires next != null ==> next.Valid() && !(this in next.footprint); modifies this; ensures Valid(); ensures next != null ==> content == [val] + next.content && footprint == {this} + next.footprint; ensures next == null ==> content == [val] && footprint == {this}; { this.val := val; this.next := next; if (next == null) { this.footprint := {this}; this.content := [val]; } else { this.footprint := {this} + next.footprint; this.content := [val] + next.content; } } }