[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 2 Jun 2016 11:07:32 -0700 (PDT)*References*: <82bc09bd-c5b9-4d2e-86d9-bfe4e86e4083@googlegroups.com>

To use a temporal logic you need a temporal modality, i.e. a machine. In TLA, the machine is explicit. What you have is a specification of three mathematical functions, not a machine. You can describe the stack itself as a machine (that interprets "push", "pop" and "top"), which in TLA(+), would require s to be a variable, say, a sequence, which you can then hide with the temporal existential operator. Alternatively, you can keep push/pop/top as functions or operators, and describe just your theorem as a machine. The specification of your theorem would contain the constant N, which is the number of push/pop operations. You would then initialize two variables, m and n in the starting state to N, and in each step, nondeterministically do a push or a pop, decrementing m or n respectively until they reach zero.

**References**:**pvs, temporal logic and stacks***From:*fl

- Prev by Date:
**pvs, temporal logic and stacks** - Next by Date:
**Re: pvs, temporal logic and stacks** - Previous by thread:
**pvs, temporal logic and stacks** - Next by thread:
**Re: pvs, temporal logic and stacks** - Index(es):