EECS 755

Software Requirements Modeling and Analysis

Index
Blog

Project 2

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.

Note that 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.

Problem 1

  1. Define push, pop, top, and isEmpty operations for the NatStack.
  2. Using Coq comments, define preconditions, postconditions, and invariants for each operation.
  3. For each function, prove your invariants and postconditions. Remember that any preconditions you define can be used as assumptions for postconditions.

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.

Problem 2

  1. Define push, pop, top, and isEmpty for a Stack that is parameterized over the stack element.
  2. Redo your proofs from Problem 1.
  3. Using a Coq example, explain why (pop (pop (push y (push x empty)))) is safe and will not crash for arbitrary x and y.
  4. Using a Coq example, explain why (pop (pop (push x empty)) is unsafe, but will not crash for arbitrary x.

Problem 3

  1. Define push, pop, top and isEmpty again for your parameterized Stack type moving the runtime checks into the type system.
  2. Redo your proofs from Problem 1.
  3. Using a Coq example, explain why (pop (pop (push y (push x empty)))) is safe and will not crash for arbitrary x and y.
  4. Using a Coq example, explain why (pop (pop (push x empty)) is unsafe, but will not crash for arbitrary x. (Hint: Show it will never run.)