Abstract Commands: A Uniform Notation for Specifications and Implementations

AbstractTotal correctness and general correctness are examined, and the latter is promoted as the more appropriate semantic basis for the programs which comprise the basic sequential interacting components of today's typically highly distributed systems, for which at certain times non-termination may actually be required. To this end we present a new abstract programming language, our abstract command language, defined with a full general-correctness semantics, and an appropriate notion of refinement which preserves general correctness and in respect of which all the constructors of our language are monotonic.This provides a uniform notation for an abstract specification which expresses such a non-termination requirement and its stepwise and piecewise refinement into an executable implementation which meets such a requirement. Moreover, we illustrate the use of one of our language's constructors, concert, which enables such non-termination requirements to emerge during piecewise refinement, and we describe its implementation via a primitive form of concurrency