A Logic for Correct Program Development |
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 B₂ bool boolean expressions bound variables chapter complete components Computer Science conclusion Constable constructive correct program development defined describes Dijkstra element type Elspas environment et.al example executable exp₁ exp₁exp₂ exp₂ extraction extractor formal formula free name free variables global variables Hoare hypotheses imperative programs implementation integer interpretation invocation iter iter X itery justification transformer justifies V(iter lemma loop manipulate meaning method methodology natural deduction occur predicate presented proc(G from H produced program segment program verification programming languages proof omitted proposition provides reasoning recursive refinement logics refinement rules sequent calculus set theory set(T specification language subgoal substitution syntactic synthesis techniques thesis top down development transition specification trivial justification true tuples type parameters valid var-list variable names verification well-formed Wirth X[s p X[S pr yields