(F : Flag) rev rev F = Fbecause in fact rev rev F = F + 2 in this model. But it does appear to satisfy that equation, in that the flag is up or down exactly when we want it to be.
th FLAG is sort Flag . ops (up_)(dn_)(rev_) : Flag -> Flag . op up?_ : Flag -> Bool . var F : Flag . eq up? up F = true . eq up? dn F = false . eq up? rev F = not up? F . endth
obj NFLAG is pr EVENAT *(sort Nat to Flag) . ops (up_)(dn_)(rev_) : Flag -> Flag . op up?_ : Flag -> Bool . var F : Flag . eq up F = 2 * F . eq dn F = 2 * F + 1 . eq rev F = F + 1 . eq up? F = even(F) . endo
For another example, the usual implementation of a stack by an array and a pointer does not literally satisfy the equation
(S : Stack) ( N : Nat) pop push(N,S) = Sbut it does behaviorally satisfy that equation, in the sense that any visible consequence of that equation is literally satisfied. Thus, we need a technique for proving behavioral properties of specifications, and in particular behavioral satisfaction of equations. The technical definition of behavioral satisfaction is a cornerstone of hidden algebra; the idea was originally given by Horst Reichel in a different setting (partial algebras without hidden sorts). Here is our version:
Given a hidden signature and a model M and an equation over that signature, we say that M behaviorally satisfies the equation, written
M ( X) t1 = t2if and only if
M ( X) c[t1] = c[t2]for every context c, which is a term of visible sort having just one variable of hidden sort, for which the term inside brackets is substituted, and where indicates ordinary satisfaction.