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 to 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 of programs, and Scott's induction.