## Correctness preserving program refinements: proof theory and applications |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

INTRODUCTION | |

DESCRIBING STATE TRANSFORMATIONS | 15 |

REFINEMENT AND WEAKEST PRECONDITIONS | 27 |

5 other sections not shown

### Common terms and phrases

abort ALGOL 60 assertions assignment statement Assume assumption atomic description axiom bounded nondeterminacy chapter Computer Science condition construction control structures correct refinement countable set data space deduction theorem defined denoted DIJKSTRA 15 distinct variables equivalent example F V,V F V,W F.L. Bauer first-order logic follows formal formula gives holds implementation induction inference rules infinitary logic initial int S,V ISBN 90 iteration J.H. VAN LINT k-place predicate symbol KARP 27 legal description Lemma list of distinct loop Lu.u non-logical symbol nondeterministic assignment occurring program description program development program transformation rules proof rule prove refinement between descriptions refinement relation refinement step replacement representational abstraction result rule for refinement S S S satisfying Section 6.1 set of sentences set of variables skip stepwise refinement technique Theorem 5.4 tion total correctness tt iff V-assignment var(Q weak termination weakest preconditions WP(S y=yQ