Behavioral Satisfaction
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 behaviorally satisfy that equation, in the sense that any visible consequence of that equation is literally satisfied.

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  e  
if 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>