Project 2 involves the construction of several modules defining stacks.
Start with these inductive types for defining the structure representing stacks and stack values:
Inductive SC : Type := | Value : nat -> SC | Unknown : SC. Inductive NatStack : Type := | Empty : NatStack | Add : nat -> NatStack -> NatStack.
Add is just the push constructor, but I’ve named it
Add to avoid confusion in the specification when we start talking about the
push operator. Feel free to add
Notation definitions should you desire.
isEmptyoperations for the
All operations will have postconditions, but not all operations will have preconditions and invariants. Your functions should implement runtime checks to make sure they do not crash for any input.
Stackthat is parameterized over the stack element.
(pop (pop (push x empty))is unsafe, but will not crash for arbitrary x.
isEmptyagain for your parameterized
Stacktype moving the runtime checks into the type system.
(pop (pop (push x empty))is unsafe, but will not crash for arbitrary x. (Hint: Show it will never run.)