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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Tue, 31 May 2016 10:24:00 -0700 (PDT)

Having a look at PVS, ( a nice system but with no temporal logic embedded)

> http://pvs.csl.sri.com/

and reading in their tutorials the pages where a stack is specified

> http://www.csl.sri.com/papers/wift-tutorial/wift-tutorial.pdf (p. 44)

I have come across axioms like

> top(push(x, s)) = x

or

> pop(push(x, s)) = s

and theorems like

> pop(pop(push(x, push(y, s)))) = s

so far so good. But it comes to my mind that the style of theorems you really want would be better

> if you push an x and then applies any sequence of "push" and "pop" ("push" and "pop" in equla number)

> you will retrieve your x with "top".

And I think that you need a temporal logic to express (easily) this property. But I don't

exactly know which one?

So it is my question: WHICH ONE?

(To tell the truth I suppose with a sequence of "push" and "pop" we can express this theorem in PVS but

with a temporal logic it would look more natural).

--

FL

**Follow-Ups**:**Re: pvs, temporal logic and stacks***From:*Leslie Lamport

**Re: pvs, temporal logic and stacks***From:*Ron Pressler

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