It is common for software engineers to write clever code that does not satisfy its specification, but always "appears" to do so. A simple (and not so clever) example is the model with natural number states NFLAG of the FLAG specification (see below), which does not satisfy the equation

(F : Flag) rev rev F = Fbecause in fact rev rev F = F + 2 in this model. But it does

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

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

[Next] [Prev] [Home] [BHome]

12 October 1996