Proving program inclusion using Hoare's logic
Publication date
1984
Authors
Bergstra, J.A.
Klop, J.W.
Editors
Advisors
Supervisors
DOI
Document Type
Article
Metadata
Show full item recordCollections
License
Abstract
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.
Keywords
Data type specification, program correctness, program equivailence, conservative refinement, program inclusion, prototype proof, logical completion