The Theory and Practice of Refinement: Approaches to the Formal Development of Large-scale Software SystemsJohn McDermid Updated proceedings of a workshop on the title subject held at York, England, January 1988. Explores the management of complex, large-scale industrial software systems through the use of a hierarchy of specifications, each progressively more detailed. Centers around the major problems of consistency, of proceeding from a high to a low level of specificity, and verification of the proper route. The 11 papers are research oriented, but should be understandable to most practitioners working with formal methods. Topics include interactive and shared systems, process refinement, data reification, program construction, and several case studies. Of interest to software researchers and those wishing to apply refinement techniques to an industrial situation. No index. Annotation copyrighted by Book News, Inc., Portland, OR |
Contents
Introduction | 1 |
Refinement of Shared Systems | 27 |
Experience of Formal Development in CICS | 59 |
Copyright | |
4 other sections not shown
Common terms and phrases
abstract data type abstract specification algorithm Areg array B_def behaviour borrower C_file C_index C_RECORD C.A.R. Hoare checked checked_out Communicating Sequential Processes components copy correctness data refinement data type defined definition denote dinv-Add(st divergences(Q Doc1 Doc2 document domPa downward simulation equivalent error example floating point floating point unit formal development formal methods formal specification function guarded command language Hoare implementation initial initialisation interactive systems interface drift invariant Keble Road Largest INTExp last_checked_out Lemma loop machine maxbooks microcode module n(st n(sto occam p(st paper PERSON posmin post-condition Pre[A precondition predicate produced programming language Programming Research Group proof obligations prove record refinement rules reification relation requirements Retrieve retro st s(st schema semantics sequence sequential set of Comp st₁ staff Startin step structure techniques theorem tion transactions transformation users variables