On the Completeness of the Inductive Assertion Method*

Manna's theorem on (partial) correctness of programs essentially states that in the statement of the Floyd inductive assertion method, "A flow diagram is correct with respect o given initial and final assertions if suitable intermediate assertions can be found, " we may replace "if " by "if and only if. " In other words, the method is complete. A precise formulation and proof for the flow chart case is given. The theorem is then extended to programs with (parameterless) recursion; for this the structure of the intermediate assertions has to be refined considerably. The result is used to provide a characterization of recursion which is an alternative to the minimal fixed point characterization, and to clarify the relationship between partial and total correctness. Important tools are the relational representation f programs, and Scott's induction. 1