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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 3 Jun 2016 01:55:12 -0700 (PDT)*References*: <82bc09bd-c5b9-4d2e-86d9-bfe4e86e4083@googlegroups.com> <cb211369-98e3-47a9-88e2-d99e63700f1b@googlegroups.com>

Thinking that this kind of abstraction is better is rather silly,

since the two ways of defining stack are isomorphic and one can define

the "concrete" representation in terms of the "abstract" one.

I didn't know that. Very interesting.

Your post and the other ones raise many questions. I'm realizing that the style of specification

is worth thinking.

You need an additional requirement--e.g., it's not true if you perform

all the pops first. Perhaps this illustrates the difficulty of using

algebraic specification.

OK. I just wanted to give a light sketch of the theorem I had in mind.

--

FL

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

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

- Prev by Date:
**Re: [tlaplus] pvs, temporal logic and stacks** - Next by Date:
**Re: [tlaplus] pvs, temporal logic and stacks** - Previous by thread:
**Re: [tlaplus] pvs, temporal logic and stacks** - Next by thread:
**specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface** - Index(es):