A General Completeness Result in Refinement


Kinoshita, Y. and Power, J., 2000. A General Completeness Result in Refinement. Heidelberg: Springer, pp. 201-218. (Lecture Notes in Computer Science)

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.


In a paper in 1986, Hoare, He and Sanders proposed a formulation of refinement for a system equivalent to the ν-calculus using a relation based semantics. To give a proof method to show that one program is a refinement of another, they introduced downward simulation and upward simulation, but the proof method based upon either of them is not complete with respect to their notion of refinement, so they claimed “joint” completeness based upon both notions of simulation with respect to their notion of refinement. We give a new definition of refinement in terms of structure respecting lax transformations, and show that the proof method based upon downward simulation is complete with respect to this notion of refinement. Although our theory works for the ν-calculus, we present the result for the μ-calculus to make the presentation simpler. We use results in enriched category theory to show this, and the central notion here is that of algebraic structure on locally ordered categories, not on sets. Our definition of refinement is neither a restriction nor a generalisation of Hoare, He and Sanders’ definition, but we include all their important examples.


Item Type Conference or Workshop Items (UNSPECIFIED)
CreatorsKinoshita, Y.and Power, J.
DepartmentsFaculty of Science > Computer Science
ID Code26472


Actions (login required)

View Item