Technical Reports by Ian Hayes

[1] IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Laws and semantics for rely-guarantee refinement. Technical Report CS-TR-1425, School of Computing Science, Newcastle University, July 2014. Superseded by [?] and other papers. 66 pages. [bib]
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
[2] IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Reasoning about concurrent programs: Refining rely-guarantee thinking. Technical Report CS-TR-1395, School of Computing Science, Newcastle University, September 2013. Superseded by CS-TR-1425. 66 pages. [bib]
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
[3] I.J. Hayes, A.Burns, B.Dongol, and C.B. Jones. Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, School of Computing Science, Newcastle University, September 2011. [bib]
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
[4] Alan Burns, Kun Wei, Jim Woodcock, IanJ. Hayes, and CliffB. Jones. Timebands framework -- 2011. Technical Report YCS-2011-467, Department of Computer Science, University of York, 2011. 36 pages. [bib]
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.
[5] R.Colvin and I.J. Hayes. A semantics for behavior trees. ACCS Technical Report ACCS-TR-07-01, ARC Centre for Complex Systems (ACCS), April 2007. [bib| http]
[6] Brijesh Dongol and IanJ. Hayes. Trace semantics for the Owicki-Gries theory integrated with the progress logic from unity. Technical Report SSE-2007-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2007. [bib]
[7] Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental semantic evaluation for interactive systems: Inertia, pre-emption, and relations. Technical Report SSE-2005-01, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib]
[8] Phil Cook, Jim Welsh, and IanJ. Hayes. Building a flexible incremental compiler back-end. Technical Report SSE-2005-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib]
[9] A.Burns, I.J. Hayes, G.Baxter, and C.J. Fidge. Modelling temporal behaviour in complex socio-technical systems. Technical Report YCS390, University of York, 2005. [bib| .html| .pdf]
[10] IanJ. Hayes. Block-structured (attribute) grammars. Technical Report 02-47, Software Verification Research Centre, The University of Queensland, December 2002. [bib]
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.
[11] Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental context-sensitive evaluation in context. Technical Report 02-11, Software Verification Research Centre, The University of Queensland, 2002. [bib]
[12] I.J. Hayes, R.Nickson, P.Strooper, and R.Colvin. A declarative semantics for logic program refinement. Technical Report 00-30, Software Verification Research Centre, The University of Queensland, Brisbane 4072, Australia, November 2000. [bib]
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.
[13] Report ofthe Computer Science Action LearningGroup. Improving the quality of tutorial classes in computer science. Technical Report UQ-CS-322, Department of Computer Science, University of Queensland, 1995. [bib]
[14] I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. Technical report UMCS-93-8-1, Department of Computer Science, University of Manchester, August 1993. [bib| .ps]
[15] I.J. Hayes. Specifying physical limitations: A case study of an oscilloscope. Technical report 167, Department of Computer Science, University of Queensland, July 1990. [bib| .ps]
[16] R.Duke, I.J. Hayes, and G.A. Rose. Verification of a cyclic retransmission protocol. Technical Report UQ-CS-92, Department of Computer Science, The University of Queensland, July 1988. [bib]
[17] I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. Technical report, Department of Computer Science, University of Queensland, 1988. [bib]
[18] I.J. Hayes and K.A. Robinson. A Modula-2-based translator generator. Technical report 84, Department of Computer Science, University of Queensland, Brisbane, Australia, 1987. [bib]
[19] I.J. Hayes and K.A. Robinson. A tutorial on Llama: A Pascal-based translator generator. Technical report, Department of Computer Science, University of New South Wales, Sydney, Australia, 1982. [bib]

This file was generated by bibtex2html 1.99.

Last updated: Wed 3 Jan 2024 17:12:52 AEDT