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.
|Requirements/Specifications (acm D.2.1), Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1), Semantics of Programming Languages (acm F.3.2)|
|Software (theme 1)|
|Software Engineering [SEN]|
Bidoit, M, Hennicker, R, & Kurz, A. (2002). Observational logic, constructor-based logic, and their duality. Software Engineering [SEN]. CWI.