using Microsoft.Contracts; // Spec# does not have good support for generics; therefore, we use an integer stack here public class Stack { [Peer] Node top; // The Peer attribute is required by Spec#'s ownership system /* Spec# proves the absence of unchecked exceptions. * Since the method does not have a throws-clause, it must not * throw checked exceptions either. */ void Push(int val) modifies this.top, top.prev; { // This implemenation has been adapted to reflect the changes in class Node, see below if(top == null) top = new Node(val); else top = top.Prepend(val); } /* The otherwise-clause gives the method the permission to throw * the declared exception when the precondition is violated. In * that case, no heap modifications are permitted. */ int Pop() requires top != null otherwise System.InvalidOperationException; modifies this.top; { if (top == null) throw new System.InvalidOperationException(); int val = top.val; top = top.next; return val; } } internal class Node { internal int val; [Peer] internal Node next, prev; // The Peer attribute is required by Spec#'s ownership system /* Spec#'s ownership system makes it somewhat complicated to link the * new node to its successor. So solve this problem, we changed the * constructor slightly and introduced the method Prepend */ internal Node(int v) { val = v; } internal Node Prepend(int v) modifies prev; ensures Owner.Same(this, result); // This postcondition is required by Spec#'s ownership system { Node t = new Node(v); expose(this) prev = t; // The expose statement is required by the Spec# methodology t.next = this; return t; } }