A refinement calculus for expressions

[摘要] This thesis describes a calculus intended for the refinement of expressions, in particular the calculus provides a framework for the formal derivation of executable expressions from initial specifications. The approach taken follows and extends the work of Back, Morris and Morgan on the refinement calculus for imperative style programs. We contribute to the area by providing a refinement calculus of expressions with a simple semantics and support for the formulation and development of specifications in parts. We take the view that a refinement calculus consists of: a specification language, which usually includes constructs which are non-executable, but is a "super-language" of a programming language; a refinement relation between specifications, which possesses particular properties necessary for the refinement of specifications in a stepwise and piecewise manner; and a set of laws determining how such refinements may proceed. We describe a simple functional language of expressions which includes features for undefinedness, non-determinism and partiality. The added constructs allow the easy formulation of expressive and abstract specifications, giving maximum freedom to the implementor. The issue of methods to structure large specifications is addressed through the concept of partiality. We provide support for the construction of specifications in parts, together with operations to compose partial specifications to form the whole. We also consider how the state and exception monads, used to hide imperative features in pure functional programs, might be used similarly to structure specifications. A refinement relation between specifications is defined. A set of laws suitable for the manipulation and refinement of expressions is proposed. The expression language is given a simple denotational semantics, using powerdomain structures to capture non-determinism. This semantics allows the easy and intuitive formal definition of refinement, using the Smyth ordering for powerdomains, and facilitates the construction of the proofs of the proposed laws for the calculus.

[发布机构] University:University of Glasgow

[关键词] Computer science