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, 2019 at 11:00

After discussing it with specialists, a standard approach would be to denote the state of the mutable stack with an immutable stack in the Hoare triples.

E.g. :

• $$[]\ s\gets create() \ [s = \mathtt{[]}]$$
• $$[s = \mathtt{SomeStack}]\ push(e, s) \ [s = \mathtt{e\mathbin{::}SomeStack}]$$
• $$[s = \mathtt{[]}]\ b\gets is\_empty(s)\ [ b = \text{True} ]$$
• $$[s = \mathtt{\_\mathbin{::}\_}]\ b\gets is\_empty(s)\ [ b = \text{False} ]$$
• $$[s = \mathtt{h\mathbin{::}t}]\ x\gets pop(s)\ [ x = h, s = \mathtt{t} ]$$

This is rather cumbersome, but it works. In a sense, it is not very different from what we do with variables in general, except that there are more than one way to change the value of a variable.

Things will get nasty if we begin to have alias problems, but this was to be expected ; separation logic is the key there.