OBSERVATIONAL SPECIFICATIONS AND THE INDISTINGUISHABILITY ASSUMPTION

To establish the correctness of some software w.r.t. its formal specif ication is widely recognized as a difficult task. A first simplificati on is obtained when the semantics of an algebraic specification is def ined as the class of all algebras which correspond to the correct real izations of the specification, A software is then declared correct if some algebra of this class corresponds to it. We approach this goal by defining an observational satisfaction relation which is less restric tive than the usual satisfaction relation. Based on this notion we pro vide an institution for observational specifications. The idea is that the validity of an equational axiom should depend on an observational equality, instead of the usual equality. We show that it is not reaso nable to expect an observational equality to be a congruence. We defin e an observational algebra as an algebra equipped with an observationa l equality which is an equivalence relation but not necessarily a cong ruence. We assume that two values can be declared indistinguishable wh en it is impossible to establish they are different using some availab le observations. This is what we call the Indistinguishability Assumpt ion. Since term observation seems sufficient for data type specificati ons, we define an indistinguishability relation on the carriers of an algebra w.r.t. the observation of an arbitrary set of terms. From a ca reful case study it follows that this requires to take into account th e continuations of suspended evaluations of observation terms. Since o ur indistinguishability relation is not transitive, it is only an inte rmediate step to define an observational equality. Our approach is mot ivated by several examples.