@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: bib2bib -ob ARTICLE.bib -oc ARTICLE-cites -c 'not $key : "TRX$"' -c '$type : "^ARTICLE$"' ../pubs-html.bib}}
@article{DRTASiaSL,
author = {Brijesh Dongol and Ian J. Hayes},
title = {Deriving real-time action systems in a sampling logic},
journal = {Sci. Comput. Program.},
publisher = {Springer Verlag},
accepted = {17 October 2011},
note = {Accepted 17 October 2011},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {TFTR},
abstract = {
Action systems have been shown to be applicable for
modelling and constructing systems in both discrete and hybrid
domains. We present a novel semantics for action systems using a
sampling logic that facilitates reasoning about the truly concurrent
behaviour between an action system and its environment. By reasoning
over the apparent states, the sampling logic allows one to determine
whether a state predicate is definitely or possibly true over an
interval. We present a semantics for action systems that allows the
time taken to sample inputs and evaluate expressions (and hence
guards) into account. We develop a temporal logic based on the
sampling logic that facilitates formalisation of safety, progress,
timing and transient properties. Then, we incorporate this logic to
the method of enforced properties, which facilitates stepwise
refinement of action systems.
},
year = 2011
}
@article{LUToPR11,
author = {I. J. Hayes and S. E. Dunne and L. A. Meinicke},
title = {Linking Unifying Theories of Program Refinement},
journal = {Science of Computer Programming},
pages = {1--27},
publisher = {Elsevier},
note = {Accepted 11 August 2011},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {TFTR},
keywords = {Unifying theories of programming (UTP), real-time refinement, program termination},
abstract = {
In this paper we consider three theories of programs and specifications at diㄦent levels of abstraction. The theories
we focus on are: the basic Unifying Theories of Programming (UTP) model, which corresponds to the theories of
VDM, B, and the refinement calculus; an extended theory that distinguishes abort from nontermination; and a further
extension that introduces (abstract) time. We define UTP-style designs (or specifications) in each theory and show
how program constructors, such as nondeterministic choice and sequential composition, can be expressed as single
designs in each theory.
To examine the relationships between the theories, we construct mappings in both directions between pairs of
theories and show that the pairs of mappings form Galois connections. This shows that the simpler (more abstract)
models are sub-theories of the more complex extensions. The mappings preserve the program structure and hence
are homomorphisms. An important property of a Galois connection is that both mappings preserve refinement. The
Galois connections between the models can be exploited to translate properties, including refinement laws, between
theories. In addition, we show how to define an iteration in the extended model in terms of an iteration in the timed
model.
},
year = {2011}
}
@article{cdsos-jalp,
author = {Robert J. Colvin and Ian J. Hayes},
title = {Structural Operational Semantics through Context-Dependent Behaviour},
journal = {Journal of Logic and Algebraic Programming},
publisher = {Elsevier},
volume = {80},
number = {7},
doi = {10.1016/j.jlap.2011.05.001},
pages = {392--426},
submitted = {25 September 2009},
revised = {10 May 2011},
accepted = {Accepted 17 May 2011},
online = {Available online 30 May 2011},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {BTLink},
abstract = {We present a new approach to providing a structural operational semantics for imperative
programming languages with concurrency and procedures. The approach is novel
because we expose the building block operations—--variable assignment and condition
checking—--in the labels on the transitions; these form the context-dependent behaviour of
a program. Using this style results in two main advantages over standard formalisms for imperative
programming language semantics: firstly, our individual transition rules are more
concise, and secondly, we are able to more abstractly and intuitively describe the semantics
of procedures, including by-value and by-reference parameters. Standard techniques in
the literature tend to result in complex and hard-to-read rules for even simple language
constructs when procedures and parameters are dealt with. Our semantics for procedures
utilises the context-dependent behaviour in the transition label to handle variable name
scoping, and defines the semantics of recursion without requiring additional rules. In contrast
with Plotkin’s seminal structural operational semantics paper, we do not use locations
to describe some of the more complex language constructs. Novel aspects of the abstract
syntax include local states (in contrast to a single global store), which simplifies the reasoning
about local variables, and a command for dynamically renaming variables (in contrast
to mapping variables to locations), which simplifies the reasoning about the effect of procedures
on by-reference parameters.},
year = {2011}
}
@article{bt-sem-scp,
author = {R. J. Colvin and I. J. Hayes},
title = {A Semantics for {Behavior Trees} Using {CSP} with Specification Commands},
journal = {Science of Computer Programming},
publisher = {Elsevier},
volume = {76},
number = {10},
doi = {10.1016/j.scico.2010.11.007},
url = {http://www.sciencedirect.com/science/article/pii/S0167642310002066},
pages = {891--914},
issn = {0167-6423},
accepted = {Accepted 15 Nov 2010},
online = {Available online 9 December 2010.},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {BTLink},
abstract = {In this paper we give a formal definition of the requirements translation language Behavior Trees. This
language has been used with success in industry to systematically translate large, complex, and often
erroneous requirements documents into a structured model of the system. It contains a mixture of state-based
manipulations, synchronisation, message passing, and parallel, conditional, and iterative control structures.
The formal semantics of a Behavior Tree is given via a translation to a version of Hoare's process algebra CSP,
extended with state-based constructs such as guards and updates, and a message passing facility similar
to that used in publish/subscribe protocols. We first provide the extension of CSP and its operational
semantics, which preserves the meaning of the original CSP operators, and then the Behavior Tree notation
and its translation into the extended version of CSP.},
keywords = {Structural operational semantics},
keywords = {Communicating Sequential Processes (CSP)},
keywords = {Hierarchical state},
keywords = {Specification commands},
keywords = {Process algebras},
keywords = {Behavior Trees},
keywords = {Requirements modelling},
year = {2011}
}
@article{ATBFfMRTS,
author = {Alan Burns and Ian J. Hayes},
title = {A Timeband Framework for Modelling Real-Time Systems},
journal = {Real-Time Systems},
publisher = {Springer Verlag},
volume = {45},
number = {1--2},
pages = {106--142},
issn = {0922-6443 (Print) 1573-1383 (Online)},
accepted = {Accepted for publication 19 March 2010},
online = {Published online 20 April 2010},
url = {http://www.springerlink.com/content/100334/?Content+Status=Accepted},
doi = {10.1007/s11241-010-9094-5},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
project = {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, it is desirable to explicitly identify distinct time
bands in which the system is situated. Such a framework enables the temporal
properties and associated dynamic behaviour of existing systems to be described and the
requirements for new or modified systems to be specified. A system model based on
a finite set of distinct time bands is motivated and developed in this paper.
},
keywords = {Real-time systems, time bands},
month = {June},
year = {2010}
}
@article{ARfPASaWL,
author = {Larissa Meinicke and Ian J. Hayes},
title = {Algebraic reasoning for probabilistic action systems and while-loops},
journal = {Acta Informatica},
publisher = {Springer Verlag},
volume = {45},
number = {5},
odoi = {dx.doi.org/10.1007/s00236-008-0073-4},
pages = {321--382},
issn = {0001-5903},
accepted = {Accepted for publication 10 March 2008},
doi = {10.1007/s00236-008-0073-4},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
xrfcd = {280302 (Software Engineering)},
xseo = {700199 (Computer Software and Services n.e.c.)},
project = {FTRT},
abstract = {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},
year = {2008}
}
@article{CMiCLPR,
author = {R. Colvin and I.J. Hayes and P.A. Strooper},
title = {Calculating modules in contextual logic program refinement},
journal = {Theory and Practice of Logic Programming},
editor = {A. Bossi},
publisher = {Cambridge University Press},
doi = {10.1017/S1471068407003043},
url = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=1459272&fulltextType=RA&fileId=S1471068407003043},
eprint = {http://journals.cambridge.org/article\_S1471068407003043},
volume = {8},
number = {01},
pages = {1--31},
for = {080309 (Software Engineering)},
seo = {890299 (Computer Software and Services not elsewhere classified)},
xrfcd = {280302 (Software Engineering)},
xseo = {700199 (Computer Software and Services n.e.c.)},
project = {RefLP/ACCS},
abstract = {
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 \emph{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 \emph{module refinement}.
A \emph{module} is a collection of procedures that operate
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
\emph{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},
year = {2008}
}
@article{PaPitRTPRC,
author = {I. J. Hayes},
title = {Procedures and Parameters in the Real-time Program Refinement Calculus},
journal = {Science of Computer Programming},
issn = {0167-6423},
volume = {64},
number = {3},
month = {February},
pages = {286--311},
doi = {10.1016/j.scico.2006.06.002},
project = {FTRT/CRTR},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
abstract = {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},
year = {2007}
}
@article{ZVDM06,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
journal = {{FACS} {FACTS}},
pages = {56--78},
title = {Understanding the differences between {VDM} and {Z}},
volume = {2006-2},
year = 2006
}
@article{ATfETDiRTP,
author = {K. Lermer and C. J. Fidge and I. J. Hayes},
title = {A Theory for Execution Time Derivation in Real-time Programs},
journal = {Theoretical Computer Science},
issn = {0304-3975},
volume = {346},
number = {1},
month = {November},
pages = {3--27},
snote = {Special issue on Quantitative Aspects of Programming Languages},
project = {TPA/CRTR/ACCS},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
year = {2005},
abstract = {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}
}
@article{LAoETC,
author = {K. Lermer and C.J. Fidge and I.J. Hayes},
title = {Linear Approximation of Execution-Time Constraints},
journal = {Formal Aspects of Computing},
volume = {15},
number = {4},
month = {December},
pages = {319--348},
trnumber = {02-31},
xnote = {in Special Issue on Semantic Foundations of Engineering Design Languages},
project = {TPA/CRTR},
year = {2003},
abstract = {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.}
}
@article{aRCfLP,
author = {I. J. Hayes and R. Colvin and D. Hemer and P. A. Strooper and R. Nickson},
title = {A Refinement Calculus for Logic Programs},
journal = {Theory and Practice of Logic Programming},
volume = {2},
number = {4--5},
month = jul,
dates = {July--September},
pages = {425--460},
issn = {?},
project = {RefLP},
year = {2002},
abstract = {
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 {\em 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.}
}
@article{RaRTRTaN,
title = {Reasoning about Real-Time Repetitions: Terminating and Nonterminating},
author = {I. J. Hayes},
journal = {Science of Computer Programming},
publisher = {Elsevier},
ocity = {Amsterdam},
volume = {43},
number = {2--3},
pages = {161--192},
pdf = {../Papers/iloop.pdf},
issn = {0167-6423},
keywords = {Real-time refinement; nonterminating repetitions.},
url = {http://www.elsevier.com/locate/scico},
rfcd = {280302 (Software Engineering)},
seo = {700199 (Computer Software and Services n.e.c.)},
project = {HertZ},
year = {2002},
abstract = {
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.}
}
@article{AItRTOZ,
author = {G. Smith and I. J. Hayes},
title = {An Introduction to {Real-Time Object-Z}},
journal = {Formal Aspects of Computing},
issn = {0934-5043},
volume = {13},
number = {2},
month = {May},
pages = {128--141},
special = {Selected papers from IFM '99},
publisher = {BCS/Springer-Verlag},
city = {London},
project = {HertZ},
year = {2002},
abstract = {
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}
}
@article{SCoDCFP,
author = {I. J. Hayes and C. J. Fidge and K. Lermer},
title = {Semantic Characterisation of Dead Control-Flow Paths},
journal = {IEE Proceedings---Software},
volume = {148},
number = {6},
month = {December},
pages = {175--186},
pdf = {../Papers/dead.pdf},
anote = {Awarded the 2001/2002 \emph{Mather Premium} by the Institution of Electrical Engineers},
project = {TPA},
year = {2001},
abstract = {
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.}
}
@article{aSRTRC,
author = {I. J. Hayes and M. Utting},
title = {A Sequential Real-Time Refinement Calculus},
journal = {Acta Informatica},
publisher = {Springer},
volume = {37},
number = {6},
pages = {385--448},
pdf = {../Papers/srtr.pdf},
project = {HertZ},
year = {2001},
abstract = {
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.}
}
@article{TDC,
author = {C. J. Fidge and I. J. Hayes and G. Watson},
title = {The Deadline Command},
journal = {IEE Proceedings---Software},
volume = {146},
number = {2},
month = apr,
pages = {104--111},
ps = {../Papers/deadline.ps},
project = {TPA},
year = {1999}
}
@article{aPRT,
author = {D. Carrington and I. Hayes and R. Nickson and
G. Watson and J. Welsh},
title = {A Program Refinement Tool},
journal = {Formal Aspects of Computing},
volume = {10},
number = {2},
pages = {97--124},
ps = {../Papers/prtj.ps},
publisher = {BCS/Springer},
year = {1998}
}
@article{EPoSL,
author = {I. J. Hayes},
title = {Expressive power of specification languages},
journal = {Formal Aspects of Computing},
volume = {10},
number = {2},
pages = {187--192},
publisher = {BCS/Springer},
year = {1998}
}
@article{SCiPR,
author = {R. Nickson and I. J. Hayes},
title = {Supporting Contexts in Program Refinement},
key = {program window inference},
journal = {Science of Computer Programming},
issn = {0167-6423},
uqcall = {QA75.5 .S35},
volume = {29},
number = {3},
pages = {279--302},
year = {1997},
abstract = {
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
{\em 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
{\em program window inference\/}, to handle such contextual
information during derivations in the refinement calculus.
The idea is borrowed from a technique, called {\em window
inference\/}, for handling context in theorem proving.
Window inference is the primary proof paradigm of the {\em Ergo\/}
proof editor. This tool has been extended to mechanize refinement
using program window inference.}
}
@article{Hayes:reuse-mod,
author = {I. J. Hayes},
key = {refinement calculus; reuse; module},
title = {Supporting module reuse in refinement},
journal = {Science of Computer Programming},
issn = {0167 6423},
uqcall = {QA75.5 .S35},
volume = {27},
number = {2},
pages = {175--184},
year = {1996}
}
@article{HayesSanders:sepio,
author = {I. J. Hayes and J. W. Sanders},
title = {Specification by interface separation},
journal = {Formal Aspects of Computing},
volume = {7},
number = {4},
pages = {430--439},
pdf = {../Papers/sepio-fac.pdf},
year = {1995}
}
@article{HayesMahony-units,
author = {I. J. Hayes and B. P. Mahony},
title = {Using units of measurement in formal specifications},
journal = {Formal Aspects of Computing},
publisher = {BCS/Springer},
volume = {7},
number = {3},
pages = {329--347},
pdf = {../Papers/units.pdf},
year = {1995}
}
@article{Diff-VDM-Z-SS,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
title = {Understanding the differences between {VDM} and {Z}},
journal = {ACM Software Engineering News},
publisher = {ACM},
note = {Unrefereed. Previously published in {\em FACS Europe} \cite{Diff-VDM-Z}},
volume = {19},
number = {3},
pages = {75--81},
month = {July},
year = {1994}
}
@article{Diff-VDM-Z,
author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
title = {Understanding the differences between {VDM} and {Z}},
journal = {FACS Europe},
volume = {1},
number = {1},
pages = {7--30},
note = {Unrefereed. Also published in {\em ACM Software Engineering News}, 19(3):75--81, July 1994},
dates = {Autumn},
year = {1993}
}
@article{MahonyHayes:Mine,
author = {B. P. Mahony and I. J. Hayes},
title = {A case-study in timed refinement: A mine pump},
journal = {IEEE Trans.\ on Software Engineering},
volume = 18,
number = 9,
pages = {817--826},
pdf = {../Papers/mahony92mine.pdf},
year = {1992}
}
@article{Hayes90f,
author = {I. J. Hayes},
title = {{VDM} and {Z}: A comparative case study},
journal = {Formal Aspects of Computing},
volume = {4},
number = {1},
pages = {76--99},
pdf = {../Papers/ndb.pdf},
category = {D},
year = 1992
}
@article{Hayes89e,
author = {I. J. Hayes},
title = {Multi-Relations in {Z}: A cross between multi-sets and binary relations},
journal = {Acta Informatica},
volume = {29},
number = {1},
pages = {33--62},
pdf = {../Papers/mrelpap.pdf},
month = {February},
category = {D},
year = 1992
}
@article{HayesJones89,
author = {I. J. Hayes and C. B. Jones},
journal = {IEE/BCS Software Engineering Journal},
month = {November},
number = {6},
pages = {330--338},
title = {Specifications are not (necessarily) executable},
volume = {4},
year = {1989}
}
@article{HoareHayesEtcFull87,
author = {C. A. R. Hoare and I. J. Hayes and {He Jifeng} and C. Morgan and A. W. Roscoe and J. W. Sanders and I. H. S{\o}rensen and J. M. Spivey and B. A. Sufrin},
journal = {Communications of the ACM},
key = {full},
month = {August},
number = {8},
pages = {672--686},
title = {Laws of Programming},
volume = {30},
note = {Corrigenda: CACM 30(9):770},
year = {1987}
}
@article{Hayes86a,
author = {I. J. Hayes},
howpublished = {PRG-49},
journal = {IEEE Transactions on Software Engineering},
key = {abstract data type invariant retrival function Z},
month = {January},
number = {1},
pages = {124--133},
title = {Specification directed module testing},
pdf = {../Papers/spectest.pdf},
volume = {SE-12},
year = {1986}
}
@article{Hayes85a,
annote = {Field Hayes 1985},
author = {I. J. Hayes},
journal = {IEEE Transactions on Software Engineering},
key = {orig Z Language, CICS},
month = {February},
number = {2},
pages = {169--178},
title = {Applying formal specification to software development in industry},
pdf = {../Papers/cics-r.pdf},
volume = {SE-11},
year = {1985}
}
This file was generated by bibtex2html 1.96.
Last updated: