Proof Obligation Generation and Discharging for Recursive Definitions in VDM

摘要

A proof obligation is a theorem stating that a certain property must hold in order for a formal specification to be internally consistent. If a proof obligation can be proved, then the referred part in the specification is consistent. The generation of proof obligations to check for a specification's internal consistency is a concept that has been applicable in a VDM context for a long time. This work is extending the existing proof obligation generation capabilities with proof obligations for the termination of recursive functions. Those proof obligations can then automatically be moved over to HOL and the corresponding proofs can be carried out in that framework. Depending upon the nature of the recursion, the discharge of these proofs can be done automatically. This paper will categorise the different kinds of recursion.