Technical Reports by Ian Hayes

Interference is the essence of concurrency and it is what makes reasoning about concurrent programs difficult. The fundamental insight of rely-guarantee thinking is that stepwise design of concurrent programs can only be compositional in development methods that offer ways to record and reason about interference. In this way of thinking, a rely relation records assumptions about the behaviour of the environment, and a guarantee relation records commitments about the behaviour of the process. The standard application of these ideas is in the extension of Hoare-like inference rules to quintuples that accommodate rely and guarantee conditions. In contrast, in this paper, we embed rely-guarantee thinking into a refinement calculus for concurrent programs, in which programs are developed in (small) steps from an abstract specification. As is usual, we extend the implementation language with specification constructs (the extended language is sometimes called a wide-spectrum language), in this case adding two new commands: a guarantee command (guar g ·c) whose valid behaviours are in accord with the command c but all of whose atomic steps also satisfy the relation g, and a rely command (rely r ·c) whose behaviours are like c provided any interference steps from the environment satisfy the relation r. The theory of concurrent program refinement is based on a theory of atomic program steps and more powerful refinement laws, most notably, a law for decomposing a specification into a parallel composition, are developed from a small set of more primitive lemmas, which are proved sound with respect to an operational semantics.

Keywords: rely-guarantee, concurrency

Interference is the essence of concurrency and it is what makes reasoning about concurrent programs difficult. The fundamental insight of rely-guarantee thinking is that stepwise design of concurrent programs can only be compositional in development methods that offer ways to record and reason about interference. In this way of thinking, a rely relation records assumptions about the behaviour of the environment, and a guarantee relation records commitments about the behaviour of the process. The standard application of these ideas is in the extension of Hoare-like inference rules to quintuples that accommodate rely and guarantee conditions. In contrast, in this paper, we embed rely-guarantee thinking into a refinement calculus for concurrent programs, in which programs are developed in (small) steps from an abstract specification. As is usual, we extend the implementation language with specification constructs (the extended language is sometimes called a wide-spectrum language), in this case adding (in addition to pre and postconditions) two new commands: a guarantee command (guar g · c) whose valid behaviours are in accord with the command c but all of whose atomic steps also satisfy the relation g, and a rely command (rely r · c) whose behaviours are like c provided any interference steps from the environment satisfy the relation r. The theory of concurrent program refinement is based on a theory of atomic program steps and more powerful refinement laws, most notably, a law for decomposing a specification into a parallel composition, are developed from a small set of more primitive lemmas, which are proved sound with respect to an operational semantics.

Keywords: rely-guarantee, concurrency

Expression evaluation in programming languages is normally deterministic; however, if expressions involve variables that are being modified by the environment of the process during their evaluation, the result of the evaluation can be nondeterministic. Two common cases where this occurs are in concurrent programs where processes share variables and real-time programs that interact to monitor and/or control their environment. In these contexts, while any particular evaluation of an expression gives a single result, there is a range of possible results that could be returned depending on the relative timing of modification of variables by the environment and their access within expression evaluation. Hence to model the semantics of expression evaluation one can use the set of possible values the expression evaluation could return. This paper considers three views of interpreting expressions nondeterministically. The paper formalises the three approaches, highlights different properties satisfied by the approaches, relates the approaches and explores conditions under which they coincide. Furthermore, a link is made to a new notation used in reasoning about interference.

Keywords: sampling logic

Complex real-time systems must integrate physical processes with digital control, human operation and organisational structures. New scientific foundations are required for specifying, designing and implementing these systems. One key challenge is to cope with the wide range of time scales and dynamics inherent in such systems. To exploit the unique properties of time, with the aim of producing more dependable computer-based systems, a timeband framework has been developed. In this paper we review this framework and report on modifications, extensions and applications that have been undertaken in funded research that completed in 2011.

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.

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.