= Solution
Use an abstract finite <sequence> $s$ of <integers>, initially empty. In the following <trait>, comments are the mathematical specification; $s_0$ means the abstract state on entry, and `result` means the returned value.
``
trait ReversableBuffer {
// Abstract state s: finite sequence of Int, initially [].
// Pre: true. Post: s = s0 ++ [x].
def append(x: Int): Unit
// Pre: true. Post: s = [x] ++ s0.
def prepend(x: Int): Unit
// Pre: 0 <= i < length(s0).
// Post: result = s0 !! i,
// s = take i s0 ++ drop (i+1) s0.
def get(i: Int): Int
// Pre: true. Post: s = reverse(s0).
def rev: Unit
}
``
The <postcondition> of `get` includes removal: it is not merely indexed reading. In particular,
$$
\boxed{\operatorname{get}(i)\text{ returns }s_{0,i}\text{ and deletes exactly that occurrence}.}
$$
Repeated equal values elsewhere in the <sequence> remain present. <List concatenation>, indexing and <list reversal> in the specification describe abstract behavior without committing to a physical representation.
Back to article page
