What people are saying - Write a review
We haven't found any reviews in the usual places.
Correct program development by formal refinement
A logic for correct program development
The extraction of programs from proofs
4 other sections not shown
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