Correctness of Programs with Function Procedures

摘要

The correctness of programs with programmer-declared functions is investigated. The framework of typed lambda calculus with explicit declaration of (possibly recursive) functions is used. Its expressions occur in the statements of a simple language with assignment, composition and conditionals. A denotational and an operational semantics for this language are provided, and their equivalence is proven. A proof system for partial correctness is presented and its soundness is shown. Completeness is then established for the case that only call by value is allowed. Allowing call by name as well, completeness is shown only for the case that the type structure is restricted, and at the cost of extending the language of the proof system. The completeness problem for the general case remains open. In the technical considerations, an important role is played by a reduction system which essentially makes it possible to reduce expression evaluation to systematic execution of auxiliary assignments. Termination of this reduction system is shown using Tait's computability technique.