Publications by Ian Hayes

Control programs for safety-critical systems are required to tolerate faults in the devices they control. In this paper we examine a systematic approach to devising code to detect faulty devices at runtime. The approach is centred around the use of integrity constraints, which are invariants on the state of a system's variables, including its inputs and outputs. Under normal operation s should always hold, but they are designed to fail to hold if there is a fault. By adding variables to capture the previous state of variables or the time of significant events, additional integrity constraints can be devised to check for faults in state transitions or faults with the rate of progress of the system. We discuss techniques for devising integrity constraints as well as efficiently evaluating the constraints. When an error is detected via the failure of an integrity constraint, the integrity constraint(s) that failed can help diagnose the likely fault. We illustrate the approach using controller software written in the action system style, but it is equally applicable to other state machine approaches such as Event-B and TLA.

The term refinement algebra refers to a set of abstract algebra, similar to Kleene algebra with tests, that are suitable for reasoning about programs in a total-correctness framework. Abstract algebraic reasoning also works well when probabilistic programs are concerned, and a refinement algebra that is suitable for such programs has been defined. This refinement algebra does not contain a probabilistic choice operator, and has been used to define commonalities between a variety of different - both probabilistic and non-probabilistic - program models. Although it is possible to algebraically verify a large and interesting group of theorems for probabilistic programs without explicit reference to probabilistic choices, there are circumstances in which reasoning directly about probabilistic choices may be useful. In this paper we investigate how probabilistic choice may be characterised abstract-algebraically in refinement algebra. That is, we propose a new refinement algebra in which probabilistic choice, probabilistic guards and assertions may be expressed. Two operators for modelling probabilistic enabledness and termination are also introduced.

Keywords: Kleene algebra, probability, refinement algebra, total-correctness

Back and von Wright have developed algebraic laws for reasoning about loops in a total correctness framework using the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems and probabilistic while-loops. In particular we focus on developing data refinement rules for these two constructs. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible.

Keywords: Kleene algebra, probability, refinement algebra, total-correctness

The refinement calculus for logic programs is a framework for deriving logic programs from specifications. It is based on a wide-spectrum language that can express both specifications and code, and a refinement relation that models the notion of correct implementation. In this paper we extend and generalise earlier work on contextual refinement. Contextual refinement simplifies the refinement process by abstractly capturing the context of a subcomponent of a program, which typically includes information about the values of the free variables. This paper also extends and generalises module refinement. A module is a collection of procedures that operate 5B on a common data type; module refinement between a specification module A and an implementation module C allows calls to the procedures of A to be systematically replaced with calls to the corresponding procedures of C. Based on the conditions for module refinement, we present a method for calculating an implementation module from a specification module. Both contextual and module refinement within the refinement calculus have been generalised from earlier work and the results are presented in a unified framework.

Keywords: Logic programs, refinement, modules, context

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints on when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire.

For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler.

Keywords: Real-time programming; Procedures and parameters; refinement calculus

Well understood methods exist for developing programs from formal specifications. Not only do such methods offer a precise check that certain sorts of deviations from their specifications are absent from implementations but they can also increase the productivity of the development process by careful use of layers of abstraction and refinement in design. These methods, however, presuppose a specification from which to begin the development. For tasks that are fully described in terms of the symbolic values within a machine, inventing a specification is not difficult but there is an increasing demand for systems in which programs interact with an external physical world. Here, the task of fixing the specification for the “silicon package” can be more challenging than the development itself. Such applications include control programs that attempt to bring about changes in the physical world via actuators and measure things in that external (to the silicon package) world via sensors. Furthermore, most systems of this class must tolerate failures in the physical components outside the computer: it then becomes even harder to achieve confidence that the specification is appropriate. This paper offers a systematic way to derive the specification of a control program. Furthermore, our approach leads to recording assumptions about the physical world. We also discuss separating the detection and management of faults from system operation in the absence of faults. This discussion is linked to the distinction between “normal” and “radical” design.

Back and von Wright have developed algebraic laws for reasoning about loops in the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems. In particular we focus on developing data refinement rules for probabilistic action systems. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible. In particular, our probabilistic action system data refinement rules are new.

Action systems are a framework for reasoning about discrete reactive systems. Back, Petre and Porres have extended these action sys- tems to continuous action systems, which can be used to model hybrid systems. In this paper we define a refinement relation, and develop prac- tical refinement rules for continuous action systems. The meaning of continuous action systems is expressed in terms of a mapping from continuous action systems to action systems. First, we present a new mapping from continuous action systems to action systems, such that the definition of trace refinement is correct with respect to it. Second, we present a stream semantics that is compatible with the trace semantics, but is preferable to it because it is more general. Although action system trace refinement rules are applicable to continuous action systems with a stream semantics, they are not complete. Finally, we introduce a new data refinement rule that is valid with respect to the stream semantics and can be used to prove refinements that are not possible in the trace semantics, and we analyse the completeness of our new rule in conjunction with the existing trace refinement rules.

Real-time control programs are often used in contexts where (conceptually) they run forever. Repetitions within such programs (or their specifications) may either (i) be guaranteed to terminate, (ii) be guaranteed to never terminate (loop forever), or (iii) may possibly terminate. In dealing with real-time programs and their specifications, we need to be able to represent these possibilities, and define suitable refinement orderings.

A refinement ordering based on Dijkstra's weakest precondition only copes with the first alternative. Weakest liberal preconditions allow one to constrain behaviour provided the program terminates, which copes with the third alternative to some extent. However, neither of these handles the case when a program does not terminate. To handle this case a refinement ordering based on relational semantics can be used. In this paper we explore these issues and the definition of loops for real-time programs as well as corresponding refinement laws.

We provide an abstract command language for real-time programs and outline how a partial correctness semantics can be used to compute execution times. The notions of a timed command, refinement of a timed command, the command traversal condition, and the worst-case and best-case execution time of a command are formally introduced and investigated with the help of an underlying weakest liberal precondition semantics. The central result is a theory for the computation of worst-case and best-case execution times from the underlying semantics based on supremum and infimum calculations. The framework is applied to the analysis of a message transmitter program and its implementation.

Keywords: Real-time programming; Control-flow analysis; Execution-time derivation and prediction; Predicate transformer semantics; Partial correctness

Support for program understanding in development and maintenance tasks can be facilitated by program analysis techniques. Both control-flow and data-flow analysis can support program comprehension by augmenting the program text with additional information that may either be displayed with the program or used to allow more sophisticated navigation of the program, e.g., from an identifier's use to its definition.

This paper outlines the addition of generic program analysis support to a generic, language-based, software development environment. The analysis tools are implemented in two phases: a language-dependent phase that extracts basic information from the program, such as its control-flow graph; and a language-independent phase that performs a more sophisticated analysis of the basic information. This separation allows program analysis tools to be easily generated for a new language.

In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.

Real-time software systems are rarely developed once and left to run. They are subject to changes of requirements as the applications they support expand, and they commonly outlive the platforms they were designed to run on. A successful real-time system will be duplicated and adapted to a variety of applications-it becomes a product line. Current methods for real-time software development are commonly based on low-level programming languages and involve considerable duplication of effort when a similar system is to be developed or the hardware platform changes.

To provide more dependable, flexible and maintainable real-time systems at a lower cost what is needed is a platform-independent approach to real-time systems development. The development process is composed of two phases: a platform-independent phase, that defines the desired system behaviour and develops a platform-independent design and implementation, and a platform-dependent phase that maps the implementation onto the target platform. The last phase should be highly automated. For critical systems, assessing dependability is crucial. The partitioning into platform dependent and independent phases has to support verification of system properties through both phases.

This paper defines an algorithm for predicting worst-case and best-case execution times, and determining execution-time constraints of control-flow paths through real-time programs using their partial correctness semantics. The algorithm produces a linear approximation of path traversal conditions, worst-case and best-case execution times and strongest postconditions for timed paths in abstract real-time programs. We further derive techniques to determine the set of control-flow paths with decidable worst-case and best-case execution times. The approach is based on a weakest liberal precondition semantics and relies on supremum and infimum calculations similar to standard computations from linear programming and Presburger arithmetic. The methodology is generic in that it is applicable to any executable language that can be supplied with a predicate transformer semantics and hence provides a verification basis for high level as well as assembler level execution-time analysis techniques.

Keywords: Real-time program analysis; Timing-path analysis; Timing prediction; Worst-case and best-case execution times; Automatic constraint determination.

This paper provides the syntax and semantics for a systematic approach to the problem of analysing control-flow paths in computer programs. We give an abstract syntax and a partial correctness semantics for program control-flow paths as a generic model for path analysis and constraint derivation. This approach is formally based on a predicate transformer semantics over a boolean-valued predicate space and an abstract command language. The notions of a command, dead commands, the entry and exit conditions of a command and the inverse of a command are formally defined and investigated on the base of the semantics. A notion of command refinement is introduced capturing the abstraction process in program development from specification to implementation with partial correctness. Furthermore, command-reduction theorems and characterisations for command refinement are derived using the underlying semantics. Finally we verify the equivalence of weakest liberal precondition and strongest postcondition semantics for program commands in terms of the ordering relation they define on the command language. The approach is generic in that it is applicable to any program language that can be supplied with a predicate transformer semantics.

Keywords: Control-flow path analysis; Partial correctness semantics; Path refinement; Weakest liberal precondition semantics; Strongest postconditions.

A program can be decomposed into a set of possible execution paths. These can be described in terms of primitives such as assignments, assumptions and coercions, and composition operators such as sequential composition and nondeterministic choice as well as finitely or infinitely iterated sequential composition. Some of these paths cannot possibly be followed (they are dead or infeasible), and they may or may not terminate.

Decomposing programs into paths provides a foundation for analyzing properties of programs. Our motivation is timing constraint analysis of real-time programs, but the same techniques can be applied in other areas such as program testing. In general the set of execution paths for a program is infinite. For timing analysis we would like to decompose a program into a finite set of subpaths that covers all possible execution paths, in the sense that we only have to analyze the subpaths in order to determine suitable timing constraints that cover all execution paths.

Well understood methods exist for developing programs from given specifications. A formal method identifies proof obligations at each development step: if all such proof obligations are discharged, a precisely defined class of errors can be excluded from the final program. For a class of “closed” systems such methods offer a gold standard against which less formal approaches can be measured.

For “open” systems -those which interact with the physical world- the task of obtaining the program specification can be as challenging as the task of deriving the program. And, when a system of this class must tolerate certain kinds of unreliability in the physical world, it is still more challenging to reach confidence that the specification obtained is adequate. We argue that widening the notion of software development to include specifying the behaviour of the relevant parts of the physical world gives a way to derive the specification of a control system and also to record precisely the assumptions being made about the world outside the computer.

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we extend the refinement calculus for logic programs to include higher-order programming capabilities in specifications and programs, such as procedures as terms and lambda abstraction. We use a higher-order type and term system to describe programs, and provide a semantics for the higher-order language and refinement. The calculus is illustrated by refinement examples.

We propose a method for the timing analysis of concurrent real-time programs with hard deadlines. We divide the analysis into a machine-independent and a machine-dependent task. The latter takes into account the execution times of the program on a particular machine. Therefore, our goal is to make the machine-dependent phase of the analysis as simple as possible.

We succeed in the sense that the machine-dependent phase remains the same as in the analysis of sequential programs. We shift the complexity introduced by concurrency completely to the machine-independent phase.

Real-time systems play an important role in many safety-critical systems. Hence it is essential to have a formal basis for the development of real-time software. In this chapter we present a predicative semantics for a real-time language. The semantics includes a special variable representing the current time, and uses timed traces to present the values of external input and outputs over time so that reactive control systems can be handled. Because a real-time control system may be a nonterminating process, we allow the specification of nonterminating programs and the development of nonterminating repetitions.

Most computing languages are highly structured but conventional (flat) grammars do not make that structure explicit. To address this issue, we examine adding block structure to grammars. We allow a production in a grammar to have local productions associated with it. The local productions are accessible only via that production. Local productions for one construct may be nested within local productions for higher level constructs to form a tree-structured hierarchy.

If block structuring is used with an attribute grammar one can also avoid explicit copying of inherited attributes through intermediate nodes in the parse tree that do not modify or make use of the attribute. For example, in the definition of an expression in a programming language grammar one may have an environment attribute that is identical for all nodes in the expression subtree. The explicit passing down of the environment attribute through the intermediate nodes can be avoided by allowing direct reference to the environment attribute of the top-level expression nonterminal.

Keywords: Block structure; attribute grammars; L-attribute grammars; upward remote attributes.

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.

This paper presents Real-Time Object-Z: an integration of the object-oriented, state-based specification language Object-Z with the timed trace notation of the timed refinement calculus. This integration provides a method of formally specifying and refining systems involving continuous variables and real-time constraints. The basis of the integration is a mapping of the existing Object-Z history semantics to timed traces.

Keywords: Real-time specification; real-time refinement; Object-Z; timed refinement calculus

An invariant is a constraint on a class which holds for each externally accessible state of its instances. A dynamic constraint is a dual-state property dictating before to after state behaviour that all methods must adhere to. Both invariants and dynamic constraints are of practical benefit as they allow explicit declaration of high-level behavioural constraints on a class and all its sub-classes. In this paper, formalisations of invariants and dynamic constraints are provided in the refinement calculus. Each is separated into coerced (specification) and extant (implemented or documentation) categories. Refinement rules are provided for strengthening invariants and dynamic constraints. Two separate development paths are identified: (behavioural) sub-classing and private refinement. Refining a class may violate its invariant or dynamic constraint. Sub-classing is a constrained form of refinement that maintains these properties. Revised refinement laws are provided. Private refinement is an alternative to (behavioural) sub-classing. It also maintains properties such as invariants and dynamics constraints and foregoes the constraints of sub-classing. The disadvantage is that private refinement can only be used to implement a class.

Keywords: Object-Oriented, Refinement Calculus, Invariants, History Properties

We define a language and a predicative semantics to model concurrent real-time programs. We consider different communication paradigms between the concurrent components of a program: communication via shared variables and asynchronous message passing (for different models of channels).

The semantics is the basis for a refinement calculus to derive machine-independent concurrent real-time programs from specifications. We give some examples of refinement laws that deal with concurrency.

The real-time refinement calculus is an extension of the standard refinement calculus in which programs are developed from a pre-condition plus post-condition style of specification. In addition to adapting standard refinement rules to be valid in the real-time context, specific rules are required for the timing constructs such as delays and deadlines. Because many real-time programs may be nonterminating, a further extension is to allow nonterminating repetitions.

A real-time specification constrains not only what values should be output, but when they should be output. Hence for a program to implement such a specification, it must guarantee to output values by the specified times. With standard programming languages such guarantees cannot be made without taking into account the timing characteristics of the implementation of the program on a particular machine. To avoid having to consider such details during the refinement process, we have extended our real-time programming language with a deadline command. The deadline command takes no time to execute and always guarantees to meet the specified time; if the deadline has already passed the deadline command is infeasible (miraculous in Dijkstra's terminology). When such a real-time program is compiled for a particular machine, one needs to ensure that all execution paths leading to a deadline are guaranteed to reach it by the specified time. We consider this checking as part of an extended compilation phase. The addition of the deadline command restores for the real-time language the advantage of machine independence enjoyed by non-real-time programming languages.

In real-time programming a timeout mechanism allows exceptional behaviour, such as a lack of response, to be handled effectively, while not overly affecting the programming for the normal case. For example, in a pump controller if the water level has gone below the minimum level and the pump is on and hence pumping in more water, then the water level should rise above the minimum level within a specified time. If not, there is a fault in the system and it should be shut down and an alarm raised. Such a situation can be handled by normal case code that determines when the level has risen above the minimum, plus a timeout case handling the situation when the specified time to reach the minimum has passed.

In this paper we introduce a timeout mechanism, give it a formal definition in terms of more basic real-time commands, develop a refinement law for introducing a timeout clause to implement a specification, and give an example of using the law to introduce a timeout. The framework used is a machine-independent real-time programming language, which makes use of a deadline command to represent timing constraints in a machine-independent fashion. This allows a more abstract approach to handling timeouts.

The refinement calculus for logic programs consists of a wide-spectrum language, a semantics for the language and a notion of refinement that can be used to develop programs from specifications. The wide-spectrum language includes many of the concepts found in logic programs, including sequential composition, existential quantification, disjunction, procedures and recursion. A number of non-implementable constructs, such as universal quantification, parallel conjunction, assumptions and specifications, are also included. The semantics are defined in terms of executions, describing the effect of the program constructs on the state of the program. A notion of refinement is defined, where one program refines another if it terminates more often and returns the same set of answers.

Non-determinism is supported in the language by allowing more than one answer, but in a refinement the refined program must return the same set of answers as the original program. In the traditional refinement calculus for imperative programs, there is another form of non-determinism, called demonic choice, which allows non-determinism to be eliminated during refinement. Thus, non-deterministic specifications, which give the implementer as much freedom as possible, can be refined to deterministic implementations.

In this paper, we introduce a notion of demonic non-determinism into the refinement calculus for logic programs. We extend the wide-spectrum language to include demonic, non-deterministic choice. We describe the changes to the underlying semantics and the notion of refinement that are required, and give an example that illustrates the use of demonic choice.

It is common for a real-time system to contain a nonterminating process monitoring an input and controlling an output. Hence a real-time program development method needs to support nonterminating repetitions. In this paper we develop a general proof rule for reasoning about possibly nonterminating repetitions. The rule makes use of a Floyd-Hoare-style loop invariant that is maintained by each iteration of the repetition, a Jones-style relation between the pre- and post-states on each iteration, and a deadline specifying an upper bound on the starting time of each iteration. The general rule is proved correct with respect to a predicative semantics.

In the case of a terminating repetition the rule reduces to the standard rule extended to handle real time. Other special cases include repetitions whose bodies are guaranteed to terminate, nonterminating repetitions with the constant true as a guard, and repetitions whose termination is guaranteed by the inclusion of a fixed deadline.

Keywords: Real-time refinement; nonterminating repetitions.

Many program verification, testing and performance prediction techniques rely on analysis of statically-identified control-flow paths. However, some such paths may be `dead' because they can never be followed at run time, and should therefore be excluded from analysis. It is shown how the formal semantics of those statements comprising a path provides a sound theoretical foundation for identification of dead paths.

This paper describes a deep embedding of a refinement calculus for logic programs in Isabelle/HOL. It extends a previous tool with support for procedures and recursion. The tool supports refinement in context, and a number of window-inference tactics that ease the burden on the user. In this paper, we also discuss the insights gained into the suitability of different logics for embedding refinement calculii (applicable to both declarative and imperative paradigms). In particular, we discuss the richness of the language, choice between typed and untyped logics, automated proof support, support for user-defined tactics, and representation of program states.

Keywords: Refinement, logic programming, theorem provers

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. Modules allow one to group together data types with sets of procedures that manipulate the data types. In this paper we develop a technique for refining a module to one that uses a more efficient representation of the data type. The technique places restrictions on the way procedures in the module use the data type, and on the way a program uses the module. The restrictions allow a more efficient implementation to be developed.

We present a comprehensive refinement calculus for the development of sequential, real-time programs from real-time specifications. A specification may include not only execution time limits, but also requirements on the behaviour of outputs over the duration of the execution of the program.

The approach allows refinement steps that separate timing constraints and functional requirements. New rules are provided for handling timing constraints, but the refinement of components implementing functional requirements is essentially the same as in the standard refinement calculus.

The product of the refinement process is a program in the target programming language extended with timing deadline directives. The extended language is a machine-independent, real-time programming language. To provide valid machine code for a particular model of machine, the machine code produced by a compiler must be analysed to guarantee that it meets the specified timing deadlines.

Keywords: Refinement calculus; machine-independent; real-time specification; real-time refinement; real-time programming; deadline command; timing constraint analysis; time-invariant properties.

The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. This paper presents a semantics for a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specifications constructs (general predicates and assumptions) and universal quantification. A semantics is defined for this wide-spectrum language based on executions, which are partial functions from states to states, where a state is represented as a set of bindings. This execution semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and a refinement law for introducing recursive procedures is presented.

Keywords: Logic programming, refinement.

We develop a set of laws for reasoning about real-time programs using assertions (preconditions and postconditions) in the style of Hoare. In the real-time context assertions may refer to the current time and to the value of external inputs, which are not under the direct control of the program and hence not guaranteed to be stable with respect to the passage of time (even if the program does not modify any of the variables under its control). Hence in order to reason about real-time programs, we make use of idle-invariant assertions: assertions that are invariant to just the passage of time.

Real-time program development can be split into a machine-independent phase, that derives a machine-independent real-time program from a specification, and a machine-dependent phase, that checks that the compiled program will meet its deadlines when executed on the target machine.

In this paper we extend a machine-independent real-time programming language with auxiliary variables. These are introduced to facilitate both reasoning about the correctness of real-time programs and the expression of timing deadlines, and hence the calculation of timing constraints on paths through a program. The auxiliary variable concept is extended to auxiliary parameters to procedures.

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. Modules allow one to group together data types with sets of procedures that manipulate the data types. In this paper we develop a technique for refining a module to one that uses a more efficient representation of the data type. The technique places restrictions on the way procedures in the module use the data type, and on the way a program uses the module. The restrictions allow a more efficient implementation to be developed.

It is common for a real-time process to consist of a nonterminating loop monitoring an input and controlling an output. Hence a real-time program development method needs to support nonterminating loops. Earlier work on real-time program development has produced a real-time refinement calculus that makes use of a novel deadline command which allows timing constraints to be embedded in real-time programs. The addition of the deadline command to the real-time programming language gives the significant advantage of providing a real-time programming language that is machine independent. This allows a more abstract approach to the program development process.

In this paper we add possibly nonterminating loops to the refinement calculus. First we examine the semantics of possibly nonterminating loops, and use them to reason directly about a simple example. Then we develop simpler refinement rules that make use of a loop invariant.

The logic programming refinement calculus is a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we show how types can be handled in the logic programming refinement calculus. Types of variables are necessary for a complete specification of a procedure, and typing information can guide the refinement of a procedure specification to code. As an application of this framework, we show how dynamic type-checks can be formally eliminated from a sample program.

We consider the specification and refinement of sequential real-time programs. Our real-time specifications describe the allowable behaviours of an implementation in terms of the values of variables over time. Hence within a specification the values of the variables and the times at which they have those values are intertwined. However, in a real-time program some commands are concerned with calculating the right outputs, while other commands, such as delays and deadlines, are concerned with making sure the outputs appear at the right time. During the refinement process we would like to decompose the overall problem into those aspects dealing with time and those that are purely calculation. We need refinement rules that allow us to separate these concerns. Further, given a component that is only concerned with calculation, the complexities of the real-time calculus that deal with timing behaviour are an unnecessary burden. Such calculational components can be developed more straightforwardly in the standard refinement calculus. We would like to allow the use of the untimed calculus for the development of such components. To do that we need to embed the untimed calculus within the real-time calculus.

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. One aspect of refinement is transforming the representation of data in a specification. This could be performed for efficiency reasons, or to change an abstract specification type into a data type that is in the target implementation language. This paper looks at data refinement in the refinement calculus for logic programs. Three cases for data refinement in the logic calculus are examined, and the process for each is described. The three cases are illustrated by a running example.

This paper extends the methods of the refinement calculus to allow the derivation of certain kinds of Oberon-like programs. The use of records, pointers, opaque types and type extension distinguishes the work from previous examples. A case study for a queue abstract data type illustrates a method for the derivation of a generic, linked implementation. Firstly, a sequence of integers is refined to a sequence of integer records with link pointers. The the sequence of records is refined to a generic linked list that is close to Oberon code. Pointers are facilitated by declaring an explicit local data store for each queue variable. The advantage of Oberon over Modula-2 is the ability to separate the final code into two modules - a generic queue that maintains the linked data structure invariant and an integer instantiation of the queue, using type extension. This separation of concerns (isolation of the linked data structure properties) is the main benefit of the approach.

A program can be refined either by transforming the whole program or by refining one of its components. The refinement of a component is, for the main part, independent of the remainder of the program. However, refinement of a component can depend on the context of the component for information about the variables that are in scope and what their types are. The refinement can also take advantage of additional information, such as any precondition the component can assume. The aim of this paper is to introduce a technique, which we call program window inference, to handle such contextual information during derivations in the refinement calculus. The idea is borrowed from a technique, called window inference, for handling context in theorem proving. Window inference is the primary proof paradigm of the Ergo proof editor. This tool has been extended to mechanize refinement using program window inference.

As part of a project with the aim of scaling up formal methods, we have developed a library construct for the specification language Z. This paper reports on the result of using libraries to structure a specification of a relatively complicated parser for a language-based editor. The parser is complicated by the need to cope with multiple languages as well as tolerate errors in the input. Our goal in producing the specification of the parser has been to separate each of the major concepts on which the specification is based (eg, multiple languages and error-tolerance) into a separate library. To achieve the separation of concerns we have applied the novel technique of specifying each of the major concepts of the parser as grammar transformations. The full parser can then be specified by composing the separate transformations to give a grammar incorporating all the desired features.