Inferring Program Properties in Polynomial-Time
AUTHOR: Robert Givan
ABSTRACT:
I present a simple and natural polynomial-time algorithm which
analyzes functional programs and infers interesting properties of
them. Automatically inferred properties include, for example, that
insertion-sort and merge-sort correctly return sorted permutations of
their inputs.
My algorithm generalizes the effective approaches used in standard
type inference to a much more expressive (and undecidable)
"specification language". The notion of "type" is generalized so that
any RE set is a type, without losing the efficiency of standard type
inference algorithms---we *do* lose the completeness, of course. The
willingness to accept incompleteness is perhaps the heart of this
approach, as it allows the demonstration of the effectiveness of very
simple algorithms in very hard domains.