Article,
Semantic inheritance in unifying theories of programming
Formal Aspects of Computing, (2009)
DOI: http://dx.doi.org/10.1007/s00165-007-0051-6
Abstract
Abstract This paper introduces a number of new techniques that support systematic manipulation of predicates, operators, healthiness conditions, laws and fixpoints of recursive programs. Necessary restrictions are imposed on the definition of each model so that the inheritance relation can be established by checking a few conditions on the healthiness conditions and the commands. In particular, we intend to identify the conditions that simplify the closure proof of the program operators and enable laws and fixpoints of a model to be inherited by its submodel without re-proof. A recursive program may correspond to different recursive functions in a model and its submodels, because the primitives such as abort and assignment statements are normally represented as different predicates in different models (although the original definition of each operator is unchanged). This paper studies meta-theory in this more general setting. A fixpoint theorem is discovered and applied to clarify the relationship between the partially correct relational model and the totally correct sequential model in UTP. It is shown that, although assignment statements are modified by the new healthiness conditions in the latter model, most laws (including many that are re-proved in UTP) and fixpoints can be inherited directly without re-proof, if the first argument of every sequential composition in each command tree corresponds to a terminating computation. This result also singles out a small number of laws and fixpoints that may no longer hold in the totally correct model.
