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

Re: pvs, temporal logic and stacks

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.