We address a problem of efficiency of verification condition generation for unstructured non-deterministic imperative programs. Importance of the study is based upon two arguments:
- industrial programming is very often unstructural (e.g., extensive use of “go to” in C-programs);
- program analysis techniques (like abstraction) introduce unstructural and non-deterministic control flow to programs.
In the structural deterministic case, verification condition generation is driven by the rules of axiomatic semantics that are well known due to axiomatic semantics for Pascal by A. Hoare. In this case, generation of verification condition seems to be trivial, since its complexity is linear in the number of control structures due to modularity of structured imperative programs. In contrast, in the unstructured non-deterministic case, the complexity seems a priori to be exponential in the number of operators due to the exponential number of acyclic paths through a program. We present in this paper an efficient, sound and complete verification condition generator that can be used in both cases (i.e. in unstructured non-deterministic, as well as in structural deterministic). The generator complexity is linear in the overall number of control constructs and operators.