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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 2 Jun 2016 13:34:18 -0700 (PDT)*References*: <82bc09bd-c5b9-4d2e-86d9-bfe4e86e4083@googlegroups.com>

What you have come across is an example of what's called algebraic

specification. This is a way of specifying data structures that was

popular in the 70s and 80s. I believe that most people, including I

believe most mathematicians, would describe a stack as a finite

sequence of elements and describe the operations of push, pop, and top

in terms of sequences. In algebraic specification, one starts with a

bunch of axioms on push, pop, top, and the empty stack, and defines a

stack as something you get by performing a sequence of push operations

on the empty stack. This is supposed to be better because it's more

abstract and doesn't depend on a concrete representation of a stack

as a sequence.

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. In

practice, algebraic specifications don't work for anything but a few

simple data structures like stacks. It's very hard for mathematicians

to figure out the correct set of axioms, and impossible for engineers.

I remember years ago talking to someone who worked on this kind of

specification, and he said that you should specify a small number of

primitive data types this way and define anything else "concretely" in

terms of them. You can think of TLA+ this way, where sets and

functions are defined algebraically and other data structures are

defined in terms of them. Algebraic specification seems to have

fallen out of fashion.

if you push an x and then applies any sequence of "push" and "pop"

("push" and "pop" in equal number) you will retrieve your x with

"top".

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.

As Ron pointed out, what whoever wrote that spec you found was doing

was defining a data structure, not a machine/program. For any data

structure, you can define a machine that takes its operations as input

and produces results as output. I suggest doing that for an arbitrary

data structure rather than specializing it for a stack.

Leslie

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

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

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

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