This is a very minimal introduction to Guttag’s style of specification.
I am not sure that he would recognize it.
It is the part that I remember.
(Perhaps The Larch Family of Specification Languages is a primary source.)
Most expressions in Guttag’s language denote states of an object whose behavior is being defined.
The state is itself abstract in that there are generally no operators on the object to directly query its innards, even abstractly.
The object’s behavior is constrained only by the Guttag statements that refer to its state.
Actually, depending on the object’s job, the Guttag expressions may also denote operand values in the problem domain of the object.
The definition of the stack refers to the values that are stacked.
A stack
This is the typical first example.
There are two stack operations that we must define: push and pop.
In Guttag notation, each takes a stack state as an argument.
We will define two functions for pop: popS and popV for that operation produces two results, a stack value and a new state.
The push takes a value argument.
We need just two definitional equations:
- popV(push(s, v)) = v
- says that if I push a value onto a stack, initially in state s, and then pop that stack then I get the same value back again.
- popS(push(s, v)) = s
- says that the stack returns to its original state in the same scenario.
popV(popS(push(push(s, v1), v2))) = v1 follows directly from the above equations and means that if I push two values onto a stack and then pop twice, the second pop gives me the first pushed value.
It would seem that there is nothing else to say about a stack that does not stem from the two definitional equations.
We have stack axioms!
You might want to define an operator that returns a new empty stack which is illegal to pop.
popS(newS()) is illegal.
Some notes on putting formal specifications to productive use.
Science of Computer Programming, 2(1):53-68, October 1982.
[BibTeX entry]
I have heard at least two people say after contemplating a short Guttag definition of RAM or a stack, that they had the sudden feeling that they understood RAM or the stack for the first time.
The style evidently pleases some portion of the intellect not normally involved in understanding these elementary computing objects.
Some who study cognition suggest that there are two contrasting ways of understanding, the “what-is” mode and the “how-to” modes.
The Guttag method is a what-is style as is algebra.
The stack and RAM are operational or how-to concepts.
Denotational semantics goes a step further and considers the state of the world.
At the other end of the spectrum I read a long Guttag style description of relational data base technology (Computing Surveys?).
While it was long I am aware of no other even half hearted attempt at a formal definition of so complex a system.