@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -ob TECHREPORT.bib -oc TECHREPORT-cites -c 'not $key : "TRX$"' -c '$type : "^TECHREPORT$"' ../pubs-html.bib}}
@techreport{HayesJonesColvin14TR,
author = {Ian J. Hayes and Cliff B. Jones and Robert J. Colvin},
title = {Laws and Semantics for Rely-Guarantee Refinement},
institution = {School of Computing Science, Newcastle University},
numpages = {66},
note = {Superseded by \cite{FMJournalAtomicSteps-TR} and other papers. 66 pages},
number = {CS-TR-1425},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {DP130102901 RGT/LP0989643 SPA},
keywords = {rely-guarantee, concurrency},
abstract = {
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 $(\mathbf{guar} g ~\cdot~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 $(\mathbf{rely} r ~\cdot~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.
},
month = jul,
year = {2014}
}
@techreport{RRGT-TR13,
author = {Ian J. Hayes and Cliff B. Jones and Robert J. Colvin},
title = {Reasoning about concurrent programs: Refining rely-guarantee thinking},
institution = {School of Computing Science, Newcastle University},
numpages = {66},
note = {Superseded by CS-TR-1425. 66 pages},
number = {CS-TR-1395},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {DP130102901 RGT/LP0989643 SPA},
keywords = {rely-guarantee, concurrency},
abstract = {
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 \emph{rely} relation records assumptions about
the behaviour of the \emph{environment}, and a \emph{guarantee} relation records
commitments about the behaviour of the \emph{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 $(\mathbf{guar} g ~\cdot~ 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 $(\mathbf{rely} r ~\cdot~ 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.
},
month = sep,
year = {2013}
}
@techreport{CMoNEE-TR,
author = {I. J. Hayes and A. Burns and B. Dongol and C. B. Jones},
title = {Comparing Models of Non\-deterministic Expression Evaluation},
institution = {School of Computing Science, Newcastle University},
pages = {1--21},
number = {CS-TR-1273},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {DP0987452 TFTR},
keywords = {sampling logic},
abstract = {
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 non\-deterministic.
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.
},
month = {September},
year = {2011}
}
@techreport{timebands-TR,
author = {Alan Burns and Kun Wei and Jim Woodcock and Ian J. Hayes and Cliff B. Jones},
title = {Timebands Framework -- 2011},
number = {YCS-2011-467},
pages = {1--36},
note = {36 pages},
institution = {Department of Computer Science, University of York},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {DP0987452 TFTR},
abstract = {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.},
year = {2011}
}
@techreport{TSftOGTIwtPLfU07-TR,
author = {Brijesh Dongol and Ian J. Hayes},
title = {Trace Semantics for the {Owicki-Gries} Theory Integrated with the Progress Logic from UNITY},
number = {SSE-2007-02},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
year = {2007}
}
@techreport{ASfBT-TR,
author = {R. Colvin and I.J. Hayes},
title = {A Semantics for Behavior Trees},
institution = {ARC Centre for Complex Systems (ACCS)},
type = {ACCS Technical Report},
number = {ACCS-TR-07-01},
url = {http://www.accs.edu.au/documents/TechnicalReports/ACCS_TR_07_01},
month = {April},
project = {CEO348249 ACCS},
year = {2007}
}
@techreport{BurnsEt05,
author = {A. Burns and I. J. Hayes and G. Baxter and C. J. Fidge},
title = {Modelling Temporal Behaviour in Complex Socio-Technical Systems},
year = {2005},
institution = {University of York},
url = {https://www.cs.york.ac.uk/rts/publications/Burns2005.html},
pdf = {../Papers/R_Burns_2005.pdf},
number = {YCS~390}
}
@techreport{BaFICBE05,
author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
title = {Building a Flexible Incremental Compiler Back-End},
number = {SSE-2005-02},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
year = {2005}
}
@techreport{ISEfIS05,
author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
title = {Incremental Semantic Evaluation for Interactive Systems: Inertia, Pre-emption, and Relations},
number = {SSE-2005-01},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
year = {2005}
}
@techreport{ICSEiC-TR,
author = {Phil Cook and Jim Welsh and Ian J. Hayes},
title = {Incremental Context-Sensitive Evaluation in Context},
institution = {Software Verification Research Centre, The University of
Queensland},
number = {02-11},
project = {Phil PhD},
year = {2002}
}
@techreport{BSAG-TR,
author = {Ian J. Hayes},
title = {Block-Structured (Attribute) Grammars},
institution = {Software Verification Research Centre, The University of Queensland},
number = {02-47},
month = dec,
project = {},
code = {K (Research report)},
rfcd = {280303 (Programming Languages)},
seo = {700199 (Computer Software and Services n.e.c.)},
year = {2002},
abstract = {
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.}
}
@techreport{ADSfLPR-TR,
author = {I. J. Hayes and R. Nickson and P. Strooper and R. Colvin},
title = {A Declarative Semantics for Logic Program Refinement},
number = {00-30},
institution = {Software Verification Research Centre,
The University of Queensland, Brisbane 4072, Australia},
month = nov,
keywords = {Logic programming, refinement.},
project = {A49937007 RefLP},
year = {2000},
abstract = {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
{\em 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.}
}
@techreport{Tutoring,
author = {Report of the Computer Science Action Learning Group},
title = {Improving the Quality of Tutorial Classes in Computer Science},
institution = {Department of Computer Science, University of Queensland},
number = {UQ-CS-322},
year = {1995}
}
@techreport{Diff-VDM-Z-TR,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
title = {Understanding the differences between {VDM} and {Z}},
institution = {Department of Computer Science, University of Manchester},
type = {Technical report},
number = {UMCS-93-8-1},
ps = {../Papers/UMCS-93-8-1.ps},
month = {August},
year = {1993}
}
@techreport{Hayes90b-TR,
author = {I. J. Hayes},
institution = {Department of Computer Science, University of Queensland},
title = {Specifying Physical Limitations: A Case Study of an Oscilloscope},
type = {Technical report},
number = {167},
month = {July},
pages = {17 pages},
ps = {../Papers/TR0167.ps},
year = 1990
}
@techreport{HayesNeucomWelsh88,
author = {I. J. Hayes and R. Neucom and J. Welsh},
title = {An editor for {Z} specifications},
pages = {13 pages},
institution = {Department of Computer Science, University of Queensland},
year = {1988}
}
@techreport{DukeHayesRose88,
author = {R. Duke and I. J. Hayes and G. A. Rose},
title = {Verification of a cyclic retransmission protocol},
number = {UQ-CS-92},
pages = {1--23},
institution = {Department of Computer Science, The University of Queensland},
month = {July},
year = {1988}
}
@techreport{HayesRobinson87,
address = {Brisbane, Australia},
author = {I. J. Hayes and K. A. Robinson},
institution = {Department of Computer Science, University of Queensland},
pages = {35 pages},
title = {A {Modula}-2-Based Translator Generator},
type = {Technical report 84},
year = {1987}
}
@techreport{HayesRobinson82,
address = {Sydney, Australia},
author = {I. J. Hayes and K. A. Robinson},
institution = {Department of Computer Science, University of New South Wales},
pages = {27 pages},
title = {A Tutorial on {Llama}: A {Pascal}-Based Translator Generator},
type = {Technical report},
year = {1982}
}
This file was generated by bibtex2html 1.99.
Last updated: Wed 29 Oct 2025 20:41:30 AEST
