3
$\begingroup$

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 ?

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – chi
    Apr 18 '19 at 11:00
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.