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
Meven though(
M(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
Mif and only if for every context c,
Mwhere c[e] denotes the equation resulting from substituting each side of e into c.