Abstract

This is the second in a series of papers devoted to the thorough investigation of 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 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 proof-theoretic notion of refinement