Formal semantics of a mutable/imperative stack

When introducing formal semantics for data structures, immutable stacks are a nice simple example :

• $$\mathit{is\_empty}(\mathit{create()})=\mathrm{True}$$
• $$\mathit{is\_empty}(\mathit{push}(e, s))=\mathrm{False}$$
• $$\mathit{top}(\mathit{push}(e, s)) = e$$
• $$\mathit{pop}(\mathit{push}(e, s)) = s$$

I am trying to do the same for a mutable stack structure, where the $$\mathit{push}$$ and $$\mathit{pop}$$ operations will modify a stack instead of returning one.

The way I am trying to do it is with Hoare triples. I can define the simplest ones (omitting that $$s$$ is a stack and $$e$$ an element) :

• $$[]\ s\gets create() \ [\mathit{is\_empty}(s) \text{ yields True}]$$
• $$[]\ \mathit{push}(e, s) \ [\mathit{is\_empty}(s) \text{ yields False}]$$

However I am not finding satisfactory axioms for $$\mathit{pop}$$. I could do $$[\mathit{is\_empty}(s) \text{ yields some value } b]\ \mathit{push}(e, s)\mathord{;} \mathit{pop}(s)\ [\mathit{is\_empty}(s) \text{ yields the same value } b]$$.

But this is formally only applicable when one would push and immediately pop, which is too restrictive.

With the immutable version, the same axiom (mutatis mutandis : sequence vs. composition) is acceptable because in any actual $$\mathit{pop}(s)$$ where $$s$$ is an expression that correctly denotes a non-empty stack, this expression $$s$$ can be reduced (in the sense of rewriting) to a normal form $$\mathit{push}(\cdot, \cdot)$$ and the axiom will then apply, allowing for further reduction.

This does not seem to work in the mutable/imperative case. Or does it ?

A solution would be to use properties that express the length of a stack~: pushing adds one, poping subtracts one, and expressing emptiness becomes easy. But this would not be sufficient for tracking the values of the elements ; applying the same idea would amount to having a whole immutable stack in the Hoare properties to track the mutable stack in the imperative program.

Is there a neater approach to this ?

• You probably need a way to track the full contents of the stack in our Hoare triples. It should be possible to write in your pre-post-conditions things like "the n-th pushed value is even for each n > 10". You should be able to prove $[s=(s_0,\ldots,s_n)]\ push(e,s)\ [s=(s_0,\ldots,s_n,e)]$ with your Hoare rules. – chi Apr 18 at 11:00