Functional Procedures in Higher-Order Logic

In this paper we present an approach for modelling functional procedures (as they occur in imperative programming languages) in a weakest precondition framework. Functional procedures are modelled in their full generality; thus the body of a functional procedure can be built using standard specification syntax, including nondeterminism, sequential composition, conditionals and loops. We integrate our theory of functional procedures into the existing mechanisation of the refinement calculus in the HOL system. To make formal reasoning possible, we derive correctness rules for functional procedures and their calls. We show also how recursive functional procedures can be handled according to our approach. Finally, we provide a nontrivial example of reasoning about a recursive procedure for binary search. TUCS Research Group Programming Methodology Research Group 1 Introduction A procedure is a parameterised piece of code that can be called from another program. In imperative programmin..