1
vote
Accepted
Formal semantics of a mutable/imperative stack
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{[]...
- 233
1
vote
How append, prepend, and generally insertAt work in RRB-tree
How cool is it to be in a field and an age where Jean Niklas L'orange can answer your questions? That's a great response!
Another approach to consider is to localize the "focus". The focus is ...
- 545
Only top scored, non community-wiki answers of a minimum length are eligible