[lacampbell]

I don't see why the abstract specification should mention pushing or popping at all. The abstract specification for swap is simply "swaps the first and second elements of the stack". How that's achieved doesn't seem important, and it seems odd to me to define it in terms of primitive operations it's not actually defined in terms of - unless it's some ultra minimalist Forth thing where swap isn't a primitive.