4th Refinement Workshop: Proceedings of the 4th Refinement WorkshopJoseph M. Morris, Roger C. F. Shaw |
Contents
Introductory Talk to the | 1 |
Specialising Abstract Programs | 34 |
A Refinement Case Study Using the Abstract Machine | 51 |
Copyright | |
14 other sections not shown
Other editions - View all
4th Refinement Workshop: Proceedings of the 4th Refinement Workshop ... Joseph M. Morris,Roger C. Shaw No preview available - 1991 |
Common terms and phrases
abstract abstract data type algorithm application assertions axioms behaviour binary Bool C.A.R. Hoare circuit components Computer concrete concurrent systems construct constructor correctness data refinement defined definition defn denotes derivation element empty environment equivalence ev.time example export finite formal methods formula function generalised hence implementation input instruction number interface invariant is_empty iseq Lemma logic machine mathematical maxsize min{ev module node notation notion object operational semantics operations output parameter Past post-condition postcondition Pre-order predicate procedures process algebra programming language Programming Research Group proof graphs proof lattice proof obligations properties refinement calculus refinement diagram refinement relation reification rely Rename restriction result S₁ satisfy schema semantics sequence sequential Skip Spawn specification synchronisation t₁ t₂ techniques Theorem theory traces transition true type theory variables verification Workers Z notation