It is actually very common for software engineers to write clever code that doesn't really satisfy the specification, but does always "appear to" to do so. For example, the usual implementation of stacks by an array and pointer does not literally satisfy the equation

(S : Stack)(N : Nat) pop push(N,S) = S ,but it does

For another example, consider the model of the `FLAG`

specification where states are "histories," that is, sequences of all methods
(i.e., messages) received so far. Then the state after a double reversal of
F is the sequence rev rev
F, which does not equal the sequence F.
Such an implementation (or one a little simpler) would be needed if some other
attributes were required, such as the number of methods received, or the last
method received. Actually, there is *only one* implementation (up to
isomorphism) where the equation is actually true of all reachable states!
There are infinitely many other implementations M
of `FLAG`

where the equation is literally false, but always
"appears to be true," i.e., it is observationally or **behaviorally
satisfied** by M, which we write as

M (F : Flag) rev rev F = F ,even though

M (F : Flag) rev rev F = F(ordinary satisfaction) does not hold. Thus, we have to use a technique that allows us to prove behavioral satisfaction.

The technical definition of behavioral satisfaction is one of the cornerstones of hidden algebra; the idea was originally given by Horst Reichel in a different context (partial algebras without hidden sorts). Here it is:

Given a hidden signature and a model M and a
sentence e over that signature, we say that M **behaviorally satisfies** e and we write

M eif and only if for every context c,

M c[e] ,where c[e] denotes the equation resulting from substituting each side of e into c.

[Next] [Prev] [Home]

10 October 1996 html>