|
Alessandro Avallone, Marco Benini, and Dirk Nowotka Constructive Methods in Automatic Analysis of Correctness Proofs 9th International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR), Venice 1999 AbstractWe 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. Keywords: Verification, Analysis Full description: [ps - 54 KB] [ps.gz - 24 KB]. |