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