2
$\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$
  • $\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 at 11:00

Your Answer

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

Browse other questions tagged or ask your own question.