4th Refinement Workshop: proceedings of the 4th Refinement Workshop
Springer-Verlag, 1991 - Computers - 478 pages
This volume contains the papers presented at the 4th Refinement Workshop, organised by the Formal Aspects group of the British Computer Society, and held in Cambridge on January 9-11, 1991. Refinement is the term used to describe systematic and formal methods of specifying hardware and software, and transforming the specifications into designs and implementations. The value of formal methods in producing reliable hardware and software is by now widely appreciated among both academics and many workers in industry, although such methods - and in particular their application to industrial-scale problems - are still in their infancy. This workshop brought together some of the best European workers in the field to present tutorials on the state of the art in both theory and industrial application, to describe their latest research, and to indicate future directions. The papers cover the development of both sequential and concurrent systems, and both theoretical ideas and support tools for their effective use. This volume will be of interest to researchers in formal methods, and software engineers wanting to keep track of developments in the application of formal methods in industry.
45 pages matching notation in this book
Results 1-3 of 45
What people are saying - Write a review
We haven't found any reviews in the usual places.
Introductory Talk to the
Specialising Abstract Programs
A Refinement Case Study Using the Abstract Machine
14 other sections not shown
abstract data type algorithm allow application assertions assumption axioms behaviour binary Bool C.A.R. Hoare circuit components concrete concurrent systems construct constructor correctness data refinement defined definition defn denotes derivation element empty environment eqJist equivalence ev.time example export F Event finite formal methods formula function generalised guar hence Hoare logic implementation input instruction number interface invariant is-empty Lemma List livelock logic mathematical maxsize module node notation notion object operational semantics operations output parameter parametrised Past(C,S PointModule post-condition postcondition Pre-order predicate procedures process algebra programming language Programming Research Group proof graphs proof lattice proof obligations properties prove refinement calculus refinement diagram refinement relation reification Rename restriction result satisfy schema semantics sequence sequential simulation Spawn(C synchronisation techniques Theorem theory traces transition true type theory untimed variables verification Workers