A Verified Formal Model of a VC Generator

This paper describes some modelling work carried out to inform understanding of an Ada verification system. It presents a simple formal model in Z of a refinement notation comprising a miniature, but complete, imperative programming language annotated with formal specifications. The semantics of that programming language and the notion of correctness relative to the specification annotations is defined. A semantic model of a verification condition generator is given which can be proved to be sound with respect both to the programming language semantics and to the intensional semantics of the specification annotations. The specifications and proofs were prepared using the proofpower system and all proofs have been fully machine-checked. We argue that the use of appropriate abstractions and good tools make machine-checked proof a realistic and beneficial target