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