Proving program inclusion using Hoare's logic

We explore conservative refinements of specifications. These form a quite appropriate framework for a proof theory for program inclusion based on a proof theory for program correctness. We propose two formalized proof methods for program inclusion and prove these to be sound. Both methods are incomplete but seem to cover most natural cases.

Authors

• J.A. Bergstra
• J.W. Klop

Keywords

• Data type specification
• program correctness
• conservative refinement
• program inclusion
• program equivalence
• prototype proof
• logical completion