Dependable functionality

Most of the work on proof plans has been concerned with reasoning about functional and logic programs. Recently we have been investigating the use of proof plans for reasoning about the behaviour of imperative programs. In particular we have focused on the search control issues associated with the discovery and verification of loop invariants. In terms of formal reasoning the discovery of a loop invariant is typically seen as a eureka step. The strong connection between iteration and recursion has enabled us to transfer proof plans and critics designed for reasoning about functional programs into this new domain giving some promising results [7,9]. We are currently investigating the use of proof plans in the automation of the synthesis and transformation of imperative programs from formal specifications.