An Analysis of Total Correctness Refinement Models for Partial Relation Semantics II
Moshe Deutsch · Logic Journal of IGPL · 2003
This is the second in a series of papers devoted to the thorough investigation of (total correctness) refinement based on an underlying partial relational model. This paper investigates operation refinement and data-refinement based on a weakest precondition interpretation for specifications whose semantics is given by partial relations. We consider three refinement theories based on a weakest precondition interpretation for partial relation semantics: an operation refinement theory, and theories characterising data-refinement with forward and backward simulations. We show that each of these is equivalent to a (corresponding) model-theoretic refinement theory that is based on the standard approach involving relational completion operators. In addition, we demonstrate that each of the three is also equivalent to a (corresponding) proof-theoretic notion of refinement.