Observational logic, constructor-based logic, and their duality

摘要

Observability and reachability are important concepts for formal software development. While observability concepts are used to specify the required observable behavior of a program or system, reachability concepts are used to describe the underlying data in terms of datatype constructors. In this paper we first reconsider the observational logic institution which provides a logical framework for dealing with observability. Then we develop in a completely analogous way the constructor-based logic institution which formalizes a novel treatment of reachability. Both institutions are tailored to capture the semantically correct realizations of a specification from either the observational or the reachability point of view. We show that there is a methodological and even formal duality between both frameworks. In particular, we establish a correspondence between observer operations and datatype constructors, observational and constructor-based algebras, fully abstract and reachable algebras, and observational and inductive consequences of specifications. The formal duality between the observability and reachability concepts is established in a category-theoretic setting. (C) 2002 Elsevier Science B.V. All rights reserved. [References: 40]