Description:
<jats:title>Abstract</jats:title>
<jats:p>
This paper presents a new strand of investigation which complements our previous investigation of refinement for specifications whose semantics is given by
<jats:italic>partial</jats:italic>
relations (using Z as a linguistic vehicle for this semantics). It revolves around extending our mathematical apparatus so as to continue our quest for examining mathematically the essence of the lifted-totalisation semantics (which underlies the de facto standard notion of refinement in Z) and the role of the semantic elements in model-theoretic refinement, but this time in the
<jats:italic>abortive paradigm</jats:italic>
. The analysis is given in two salient parts. In the first part, we consider the simpler framework of
<jats:italic>operation-refinement:</jats:italic>
we examine the (
<jats:italic>de facto</jats:italic>
) standard account of operation-refinement in this regime by introducing a simpler,
<jats:italic>normative</jats:italic>
theory which captures the notion of
<jats:italic>firing-conditions</jats:italic>
refinement directly in the language and in terms of the natural properties of preconditions and postconditions. In the second part, we generalise our analysis to a more intricate investigation of
<jats:italic>simulation-based</jats:italic>
<jats:italic>data-refinement</jats:italic>
. The proof-theoretic approach we undertake in the formal analysis provides us with a mathematical apparatus which enables us to examine
<jats:italic>precisely</jats:italic>
the relationships amongst the various theories of refinement. This enables us to examine the general mathematical role that the values play in model-theoretic refinement in the abortive paradigm, as well as the significance of the unique interaction of these values with the notions of
<jats:italic>lifting</jats:italic>
(of data simulations) and
<jats:italic>lifted-totalisation</jats:italic>
(of operations) in this regime. Furthermore, we generalise this mathematical analysis to a more
<jats:italic>conceptual</jats:italic>
one which also involves
<jats:italic>extreme specifications</jats:italic>
.
</jats:p>