Re: [tlaplus] pvs, temporal logic and stacks

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

P.S.

My closure axiom is unnecessary as it is covered by the first axiom for push. Also, due to my lack of algebra/logic/model-theory knowledge, I don't understand why your axiom about the uniqueness of S is necessary. Anyway, I think that this exercise proves Leslie's point about the difficulty of the algebraic/axiomatic approach for engineers (like me), not to speak of the difficulty of model-checking such specifications (BTW, are there model checkers for that approach?)

Ron