It is true that the specification stated like this commits to implementing the stack as a sequence, which may not be what you want. The abstract spec is easily obtained by hiding s and n, writingSpec == \EE s,n : SpecNow, you can implement the stack as you like and need only prove that it behaves as if there were a sequence s and counter n.
I believe that is essentially what Leslie meant when he wrote that the algebraic and the model-based styles of specifying a stack were isomorphic.