Constructive Methods in Automatic Analysis of Correctness Proofs
Alessandro Avallone, Marco Benini, Dirk Nowotka · Logic-based Program Synthesis and Transformation · 1999
We show in this contribution that an instrument from Constructive Proof Theory, the Collection Method, can be used in practice to extract information from a correctness proof. In particular, we used such a method to automatically label the source code of a program with assertions that state the minimal pre- and postconditions (wrt the correctness proof) which ensure the validity of the specification.