Observational logic, constructor-based logic, and their duality
Michel Bidoit, Rolf Hennicker, Alexander Kurz · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2002
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.