Abstract This paper presents 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 . The analysis is given in two salient parts. In the first part, we consider the simpler framework of operation-refinement: we examine the ( de facto ) standard account of operation-refinement in this regime by introducing a simpler, normative theory which captures the notion of firing-conditions 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 simulation-based data-refinement . The proof-theoretic approach we undertake in the formal analysis provides us with a mathematical apparatus which enables us to examine precisely 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 lifting (of data simulations) and lifted-totalisation (of operations) in this regime. Furthermore, we generalise this mathematical analysis to a more conceptual one which also involves extreme specifications .

Abstract This paper introduces a wide-spectrum specification logic νZ. The minimal core logic is extended to a more expressive specification logic which includes a schema calculus similar (but not equivalent) to Z, new additional schema operators, and extensions to programming and program development logics.

This paper investigates data-refinement by forward and backward simulations for model-oriented specifications whose semantics is given by partial relations. The most well-known example of such a semantics is that for Z. The standard model-theoretic characterisation of refinement is a relational approach based on totalisation and lifting. We contrast this, and relate it to, a new approach inspired by various concepts in algebraic paradigms and type theory (adapted into a framework based on classical logic) for handling nondeterminism and under specification in data-refinement. We provide a new characterisation of refinement based on extracting a set of (deterministic) "implementations", each of which models the specification in question. We examine a means by which data simulations interact with this notion and demonstrate that each of the ensuing simulation-based theories is equivalent to the corresponding standard relational characterisation of refinement.

We investigate data-refinement by backward simulation for specifications whose semantics is given by partial relations. The standard model-theoretic approach is based on totalisation and lifting. We examine this model, exploring and isolating the precise roles played by lifting and totalisation in the standard account by introducing a simpler, normative theory of backward simulation data-refinement (SB-refinement) which captures refinement directly in the language and in terms of the natural properties of preconditions and postconditions. This theory is used in conjunction with four other model-theoretic approaches to determine the extent to which the standard approach is canonical, and the extent to which it is arbitrary.

Using the language Z for more than specification is hindered by the fact that its algebra of schemas is not monotonic with respect to refinement; so specification is modular, but development is not. We isolate the reasons why Z suffers from these problems and we describe alternative models for specifications and schema operations, which are monotonic. This leads us to explore a number of theoretical and pragmatic questions: the former concern logics for modular refinement; the latter explore the use of novel schema calculi in practice.

Abstract. We show how a theory of specification refinement and program development can be constructed as a conservative extension of our existing logic for Z. The resulting system can be set up as a development method for a Z-like specification language, or as a generalisation of a refinement calculus (with a novel semantics). In addition to the technical development we illustrate how the theory can be used in practice.

Stepwise design involves the process of deriving a concrete model of a software system from a given abstract one. This process is sometimes known as refinement. There are numerous refinement theories proposed in the literature, each of which stipulates the nature of the relationship between an abstract specification and its concrete counterpart. This paper considers six refinement theories in Z that have been proposed by various people over the years. However no systematic investigation of these theories, or results on the relationships between them, have been presented or published before. This paper shows that these theories fall into two important categories and proves that the theories in each category are equivalent.

In this paper we introduce and investigate an improved kernel logic Zc for the specification language Z. Unlike standard accounts, this logic is consistent and is easily shown to be sound. We show how a complete shema calculus can be derived within this logic and in doing so we reveal a high degree of logical organization within the language. Finally, our approach eschews all non-standard concepts introduced in the standard approach, notably object level notions of substitution and entities which share properties both of constants and variables. We show, in addition, that these unusual notions are derivable in Zc and are, therefore, unnecessary innovations.

Abstract. This is the first of two related papers. We introduce a simple specification logic Z C comprising a logic and a semantics (in ZF set theory) within which the logic is sound. We then provide an interpretation for (a rational reconstruction of) the specification language Z within Z C . As a result we obtain a sound logic for Z, including a basic schema calculus.

Abstract. This is the second of two related papers. In “Revising Z: Part I - logic and semantics” (this journal) we introduced a simple specification logic Z C comprising a logic and a semantics (in ZF set theory). We then provided an interpretation for (a rational reconstruction of) the specification language Z within Z C . As a result we obtained a sound logic for Z, including the basic schema calculus. In this paper we extend the basic framework with more sophisticated features (including schema operations) and we mount a critique of a number of concepts used in Z. We further demonstrate that the complications and confusions which these concepts introduce can be avoided without compromising expressibility.

Abstract. We demonstrate that the logic contained in the draft Z standard is inconsistent.

This paper is a contribution to the formal study and analysis of vernacular forms of program derivation. Specifically, in this paper, our vernacular derivations are elementary program transformations over the natural numbers. We provide an intensional semantics for these transformations within the derivations of the elementary theory of operations and numbers, ɛON. This semantics is intensional in the sense that the computational content of a derivation associated with a transformation is equal, up to the intensional equality underlying the theory ɛON, to the computational content of the transformation itself. The interpretation enables us to underwrite the correctness of the program transformations and, further, provides an analysis of correctness by classifying, via schema, the operations available by these transformations.

Abstract We present a constructive theory of types and kinds designed with program development as the major desideratum. We show how this theory may be employed to derive programs from proofs of specifications (that is, demonstrations that specifications are satisfiable) and how the infrastructure of the theory supports the transformational development of programs in a natural way.

We examine higher-order program transformations in the context of a typed, pattern-directed, higher-order, lazy functional language. We introduce the notions of higher-order accumulation and type simulation as transformational techniques. Our main illustration of these techniques concerns the transformation of a description of a small programming language into a code generator. In this example we show how our techniques tackle important questions regarding the circumstances under which data, in a functional program, can be destructively updated with impunity.