Observational specifications and the indistinguishability assumption

AbstractTo establish the correctness of some software w.r.t. its formal specification is widely recognized as a difficult task. A first simplification is obtained when the semantics of an algebraic specification is defined as the class of all algebras which correspond to the correct realizations 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 restrictive than the usual satisfaction relation. Based on this notion we provide 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 reasonable to expect an observational equality to be a congruence. We define an observational algebra as an algebra equipped with an observational equality which is an equivalence relation but not necessarily a congruence.We assume that two values can be declared indistinguishable when it is impossible to establish they are different using some available observations. This is what we call the Indistinguishability Assumption. Since term observation seems sufficient for data type specifications, we define an indistinguishability relation on the carriers of an algebra w.r.t. the observation of an arbitrary set of terms. From a careful case study it follows that this requires to take into account the continuations of suspended evaluations of observation terms. Since our indistinguishability relation is not transitive, it is only an intermediate step to define an observational equality. Our approach is motivated by several examples