An Analysis of Operation-Refinement in an Abortive Paradigm

This paper begins a new strand of investigation which complements our previous investigation of refinement for specifications whose semantics is given by partial 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 abortive paradigm. We conside the simpler framework of operation-refinement and, thus, (at least at this stage) abstract from the complications emerging when data simulations are involved: we examine the (de facto) standard account of operation-refinement in this regime by introducing a simpler, normative theory (SP-refinement) which captures the notion of firing conditions refinement directly in the language and in terms of the natural properties of preconditions and postconditions; we then summarise our observations and link them to the particular role each of the possible extreme specifications in Z plays in the abortive paradigm - this lays the foundations to a more intricate future investigation of data-refinement in this paradigm. We conclude by providing a detailed account of future work which generalises Miarka, Boiten and Derrick's work of combining the abortive and chaotic paradigms for refinement, in our mathematical framework of ZC and ZC⊥