Mathematical theory of partial correctness

摘要

In this work we show that it is possible to express most properties regularly observed in algorithms in terms of ‘partial correctness’ (i.e., the property that the final results of the algorithm, if any, satisfy some given input-output relation). This result is of special interest since ‘partial correctness’ has already been formulated in predicate calculus and in partial function logic for many classes of algorithms.