Proofs-as-Imperative-Programs: Application to Synthesis of Contracts

Proofs-as-programs is an approach to program synthesis involving the transformation of intuitionistic proofs of specification requirements to functional programs (see, e.g., [1, 2, 12]). Various authors have adapted the proofs-as-programs to other logics and programming paradigms. This paper presents a novel approach to adapting proofs-as-programs for the synthesis of imperativeSML programs with side-effect-free return values, from proofs in a constructive version of the Hoare logic. We will demonstrate the utility of this approach by sketching how our work can be used to synthesize assertion contracts, aiding software development according to the principles of design-by-contract [8].