Completeness with finite systems of intermediate assertions for recursive program schemes : (preprint)
Krzysztof Rafal Apt, Lambert Meertens · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1977
for recursIt is proved that in the general case of arbitrary context-free schemes a program is (partially) correct with respect to given initial and final assertions if and only if a suitable finite system of intermediate assertions can be found.Assertions are allowed from an extended state space.This result contrasts with the results of DE BAKKER & MEERTENS [1], where it is proved that if assertions are taken from the original state space V, then in the general case an infinite system of intermediate assertions is needed.In the case of functional schemes (where any deterministic scheme 1s a functional one) one can take V x V for the extended state space, thus obtaining a semantical counterpart of the use of auxiliary variables.