What you have come across is an example of what's called algebraic
specification. This is a way of specifying data structures that was
popular in the 70s and 80s. I believe that most people, including I
believe most mathematicians, would describe a stack as a finite
sequence of elements and describe the operations of push, pop, and top
in terms of sequences. In algebraic specification, one starts with a
bunch of axioms on push, pop, top, and the empty stack, and defines a
stack as something you get by performing a sequence of push operations
on the empty stack. This is supposed to be better because it's more
abstract and doesn't depend on a concrete representation of a stack
as a sequence.
Thinking that this kind of abstraction is better is rather silly,
since the two ways of defining stack are isomorphic and one can define
the "concrete" representation in terms of the "abstract" one. In
practice, algebraic specifications don't work for anything but a few
simple data structures like stacks. It's very hard for mathematicians
to figure out the correct set of axioms, and impossible for engineers.
I remember years ago talking to someone who worked on this kind of
specification, and he said that you should specify a small number of
primitive data types this way and define anything else "concretely" in
terms of them. You can think of TLA+ this way, where sets and
functions are defined algebraically and other data structures are
defined in terms of them. Algebraic specification seems to have
fallen out of fashion.
if you push an x and then applies any sequence of "push" and "pop"
("push" and "pop" in equal number) you will retrieve your x with
"top".
You need an additional requirement--e.g., it's not true if you perform
all the pops first. Perhaps this illustrates the difficulty of using
algebraic specification.
As Ron pointed out, what whoever wrote that spec you found was doing
was defining a data structure, not a machine/program. For any data
structure, you can define a machine that takes its operations as input
and produces results as output. I suggest doing that for an arbitrary
data structure rather than specializing it for a stack.
Leslie