EECS 755

Software Requirements Modeling and Analysis


Runtime Checks to Type Checks

I’m getting lots of questions about the goals of Problem 3 and I think some clarification is in order.

In Problems 1 and 2 you need to account for the possibility of calling pop and top on an empty stack at runtime. Specifically, you need to check whether the input is empty and return either Unknown or a value for top and empty or a value for pop.

The best way to think about Problem 3 is to eliminate Unknown and empty as return values when the input stack is empty. Instead, prove that empty is never the input to top and pop.