Proof Techniques for Hierarchically Structured Programs

A method for describing and structuring programs
that simplifies proofs of their correctness 
is presented.  The method formally represents a program
in terms of levels of abstraction, each level 
of which can be described by a self-contained nonprocedural
specification.  The proofs, like the programs, 
are structured by levels.  Although only manual proofs
are described in the paper, the method is also 
applicable to semi-automatic and automatic proofs.  Preliminary
results are encouraging, indicating that 
the method can be applied to large programs, such as operating systems.

CACM April, 1977

Robinson, L.
Levitt, K. N.

hierarchical structure, program verification, structured
programming, formal specification, abstraction, 
and programming methodology

4.0 4.29 4.9 5.24

CA770410 JB December 29, 1977  4:53 AM

2042	4	2972
2222	4	2972
2319	4	2972
2356	4	2972
2480	4	2972
2594	4	2972
2679	4	2972
2709	4	2972
2844	4	2972
2865	4	2972
2866	4	2972
2896	4	2972
2898	4	2972
2939	4	2972
2972	4	2972
2972	4	2972
2972	4	2972
2972	4	2972
2972	4	2972
3037	4	2972
3039	4	2972
3043	4	2972
3043	4	2972
3073	4	2972
3128	4	2972
3144	4	2972
3155	4	2972
970	5	2972
2204	5	2972
2597	5	2972
2732	5	2972
2738	5	2972
2972	5	2972
2972	5	2972
2972	5	2972
3030	5	2972
2247	6	2972
2356	6	2972
2457	6	2972
2651	6	2972
2958	6	2972
2972	6	2972