Reasoning About Incompletely Defined Programs

Abstract We consider automated reasoning about recursively defined partial functions with decidable domain, i.e. functions computed by incompletely defined (or underspecified) but terminating functional programs. We define an interpreter for those programs, consider termination and investigate the semantics of incompletely defined programs. The interpreter may halt with a stuck computation, e.g. when dividing a number by zero, which represents a runtime error in a conventional programming environment. We show how so-called domain procedures are synthesized which decide the domain of incompletely defined procedures in almost all cases. As calls of domain procedures occur in proof obligations, domain procedures are optimized to make them as simple as possible. We also use domain procedures to refine the program semantics such that statements causing stuck computations do not hold. Our method to reason about incompletely defined programs is implemented in the verification tool .