Proving structured programs correct, level by level
R. Infante, U. Montanary · ACM SIGPLAN Notices · 1975
Structured programs are developed and documented using levels of “virtual machines”. Problem-oriented data structures and primitives, at each level, are programmed in terms of those at the immediately lower level, until available programming constructs are reached. We suggest to extend this technique to assertions by expanding the involved predicates level by level. Using some “level axioms” We want to be able to prove any given level correct without looking at any further expansion of the primitive predicates at that level. The advantages are: i) The programmer may use problem-oriented predicates in the assertions; ii) the demand posed on the theorem prover (if any) is very limited; iii) it is possible to replace the levels not yet programmed with functionally different routines, provided the predicates are also expanded consistently .