Shared-array double stack

Two stacks can share a fixed array by growing inwards from opposite ends. Store one stack in $[0,l)$ and the other in $[r,M)$, with representation invariant $0\le l\le r\le M$. The first top is at $l-1$, the second at $r$, and $[l,r)$ is free. The abstraction function reads the first segment backwards and the second forwards to obtain top-first lists. Push requires $l<r$; a pop requires its own stack to be nonempty. Every operation uses constant time, and either stack can use all remaining space. The bounded abstract data type must expose or specify the shared capacity restriction.