CSSE3100/7100 Reasoning about Programs
Week 11 Exercises
Exercise 11.1.
A stack is a list of elements in which addition and deletion of elements occurs only at one end, called the top of the stack.
One way to implement a stack is with a linked list. Each node in the list has a value (the element) and a pointer to the next node in the list, if any. If the node is the last in the list, then its next pointer is null.
(a) Provide a specification of a stack with methods Push (for adding an element) and Pop (for removing an element).
(b) Provide a specification of a node with methods SetNext and GetNext (for setting and getting the node's next pointer) and GetValue (for getting the node's value).
(c) Implement the classes so they can be verified in Dafny.