Pre-Galois Connection for Generic State-based Components Refinement

摘要

The technique of Galois connections has been applied successfully in many areas of computer science. By employing coalgebras as models for software components, we claim that different forms of behavior model and types of state transitions for components are instances of a single form of coalgebra in a Kleisli category. Based on the Kleisli category, the results on forward/backward morphisms and refinement of components in Set are still satisfied in this more generic framework. We propose a notion of pre-Galois connection in the context of coalgebras for refinement of state-based software components which takes into consideration not only the refinement ordering but also the dynamics of the components, and we study its properties in the Kleisli category. This notion is a powerful tool for relating a component to its refinement and for relating a component to its abstraction. Thus it provides a basis for reasoning about state-based software designs and reverse engineering.