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 preand 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 foun..