Towards an adequate notion of observation

Abstract

One can attempt to solve the problem of establishing the correctness of some software w.r.t. a formal specification at the semantical level. For this purpose, the semantics of an algebraic specification should be the class of all algebras which correspond to the correct realizations of the specification. We approach this goal by defining an observational satisfaction relation which is less restrictive than the usual satisfaction relation. 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, hence we define an observational algebra as an algebra equipped with an observational equality which is an equivalence relation but not necessarily a congruence. Since terms may represent computations, our notion of observation depends on a set of observable terms. From a careful case study it follows that this requires to take into account the continuations of suspended evaluations of observable terms. The bridge between observations and observational equality is provided by an indistinguishability relation defined on the carriers of an algebra according to the observations. In the general case, this relation is neither transitive nor a congruence.