## A logic for correct program development |

### What people are saying - Write a review

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

### Contents

Correct program development by formal refinement | 8 |

A logic for correct program development | 48 |

The extraction of programs from proofs | 126 |

4 other sections not shown

### Common terms and phrases

a.e. expressions analysis asserted program assignment axioms bool bool-exp boolean expressions bound variables chapter complete components Computer Science conclusion Constable correct program development defined definition reference denote describes Dijkstra Earley element type Elspas environment et.al example executable expj=exp2 extractor formal formula free name independence free variables global variables Hoare hypotheses imperative programs implementation int-exp integer invocation iter iter1 iterx justification transformer justifies V(iter lemma loop metatheory method natural deduction occur PL/CV predicate presented procedure constant procfG from H produced program segment Program Verification programming languages proof omitted proposition provides reasoning recursive refinement logics refinement rules sequent calculus set theory set-exp specification language structured subgoal substitution syntactic synthesis techniques thesis top down development transition specification trivial justification true tuples type parameters types in env V(iter valid var-list variable names verification well-formed yields