Repository | Book | Chapter
(2006) Algebra, meaning, and computation, Dordrecht, Springer.
The COL institution (constructor-based observational logic) has been introduced as a formal framework to specify both generation- and observation-oriented properties of software systems. In this paper we consider behavioral refinement relations between COL-specifications taking into account implementation constructions. We propose a general strategy for proving the correctness of such refinements by reduction to (standard) first-order theorem proving with induction. Technically our strategy relies on appropriate proof rules and on a lifting construction to encode the reachability and observability notions of the COL institution.
Publication details
DOI: 10.1007/11780274_18
Full citation:
Bidoit, M. , Hennicker, R. (2006)., Proving behavioral refinements of col-specifications, in K. Futatsugi, J. Jouannaud & J. Meseguer (eds.), Algebra, meaning, and computation, Dordrecht, Springer, pp. 333-354.