A Brief Study in Automating Proofs Based on a Refined Hoare-logic

This report deals with program verification based on a refined Hoare-logic which allows to handle procedure calls. A certain specification technique allows to specify these procedures by pre- and postconditions. To do that, the data model of the programming language is formalized and objects of the programming language are mapped to abstract values. Specifications can thus refer to these abstract values and describe the behavior of a procedure on a higher level of abstraction. As basic operations of the programming language can cause exceptions they are considered as procedures. This allows to specify their behavior and prove the absence of certain exceptions. The disadvantage of this approach is that procedure calls play an even more prominent role in verification. Handling procedures makes automation of correctness proofs much harder because it is not possible to compute the weakest precondition of a procedure call in most cases. Two examples show how suitable preconditions can be found. On the one hand, the enhancement of the programming logic enables our framework to deal with realistic programs by handling e. g. side-effects or recursion. On the other hand it leads to larger and more complex correctness proofs. It is shown that this additional effort can mostly be done by a verification system.     «

This report deals with program verification based on a refined Hoare-logic which allows to handle procedure calls. A certain specification technique allows to specify these procedures by pre- and postconditions. To do that, the data model of the programming language is formalized and objects of the programming language are mapped to abstract values. Specifications can thus refer to these abstract values and describe the behavior of a procedure on a higher level of abstraction. As basic operation...     »