Re: pvs, temporal logic and stacks

Even though TLA+ encourages machine specification (and, indeed, this works better for arbitrary data structures, and allows powerful use of refinement), I think that in this case, just for the sake of exercise, we can keep the algebraic/functional/denotational axiomatization, yet state the theorem in TLA. Perhaps like so:

------------------------------------------ MODULE Stack ------------------------------------------
CONSTANTS X, \* The set of elements
          S, \* The set of stacks (intentionally left abstract)
          push,
          pop,
          top

\* Algebraic structure
ASSUME /\ push \in [S \X X -> S]
       /\ pop \in [S -> S]
       /\ top \in [S -> X]

\* Algebraic axioms
ASSUME \A x \in X, s \in S :
         /\ top[push[<<x, s>>]] = x
         /\ pop[push[<<x, s>>]] = s

------------------------------------------ MODULE PushPop ------------------------------------------
EXTENDS Naturals

CONSTANTS S1, x \* initial stack and "x"

ASSUME S1 \in S /\ x \in X

VARIABLES s, n

Init == /\ s = push[<<x, S1>>]
        /\ n = 0

Next == \/ n' = n + 1 /\ \E y \in X : s' = push[<<y, s>>]
        \/ n > 0 /\ n' = n - 1 /\ s' = pop[s]

Spec == Init /\ [][Next]_<<s, n>>

THEOREM PP == Spec => [](n = 0 => top[s] = x)
====================================================================================================

PP(S1, x, s, n) == INSTANCE PushPop
THEOREM
    \A s1 \in S, x \in X : \EE s, n : PP(s1, x, s, n)!PP

====================================================================================================