Behavioral Satisfaction
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 = F `
because 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) = S `
but 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 = t2 `
if 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.
[Next] [Prev] [Home] [BHome]
12 October 1996