Let's Build a Stack¶
In this lab we will build a stack data structure and use the SPARK provers to find the errors in the below implementation.
So, what is a stack?
A stack is like a pile of dishes...
The pile starts out empty.
You add (
push) a new plate (
data) to the stack by placing it on the top of the pile.
To get plates (
data) out, you take the one off the top of the pile (
Out stack has a maximum height (
size) of 9 dishes
Pushing items onto the stack
Here's what should happen if we pushed the string
MLH onto the stack.
The list starts out empty. Each time we push a character onto the stack,
Last increments by
Popping items from the stack
Here's what should happen if we popped
2 characters off our stack & then
clear don't unset the
elements, they just change the value of
N inputs will be read from stdin/console as inputs, C to the stack.
1 <= N <= 1000
C is any character. Characters d and p will be special characters corresponding to the below commands:
p => Pops a character off the stack
d => Prints the current characters in the stack
If the stack currently has the characters "M", "L", and "H" then the program should print the stack like this:
[M, L, H]
M L H d p d p d p d
[M, L, H] [M, L] [M] 
Note that, in order to prove the code below, you need to click on the Prove button.