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

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