Constructor-based observational logic

This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. In the first part of this work, we develop the essential ingredients that are needed to define the constructor-based observational logic institution, called COL, which takes into account both the generation- and observation-oriented aspects of software systems. The underlying paradigm of our approach is that the semantics of a specification should be as loose as possible to capture all its correct realizations. We also consider the “black box” semantics of a specification which is useful to study the behavioral properties a user can observe when he/she is experimenting with the system.In the second part of this work, we develop proof techniques for structured COL-specifications. For this purpose we introduce an institution encoding from the COL institution to the institution of many-sorted first-order logic with equality and sort-generation constraints. Using this institution encoding, we can then reduce proofs of consequences of structured specifications built over COL to proofs of consequences of structured specifications written in a simple subset of the algebraic specification language Casl. This means, in particular, that any inductive theorem prover, such as e.g. the Larch Prover or PVS, can be used to prove theorems over structured COL-specifications.