Correctness Preserving Program Refinements: Proof Theory and Applications |
From inside the book
11 pages matching representational abstraction in this book
Where's the rest of this book?
Results 1-3 of 11
Common terms and phrases
A₁ abort ALGOL 60 assertions assignment statement Assume assumption atomic description B₁ B₂ bounded nondeterminacy chapter Computer Science condition correct refinement countable set D₁ deduction theorem defined denoted DIJKSTRA 15 distinct variables example F V,V F V,W F.L. Bauer fin S',V first-order logic formula gives holds implementation induction inference rules infinitary logic initial int WP ISBN 90 iteration J.H. VAN LINT J.W. DE BAKKER k-place predicate symbol KARP 27 legal description Lemma list of distinct loop Lw1w nondeterministic nondeterministic assignment occurring program description program development program transformation rules proof rule PROOF THEORY prove R₂ refinement between descriptions refinement relation refinement step replacement representational abstraction rule for refinement S₁ S₂ satisfying Section 6.1 set of sentences set of variables skip stepwise refinement Theorem 5.4 tion tt iff V-assignment val A,s weak termination weakest preconditions WP S,G(v WP S,Q y=Yo Ов