Abstract

Specification and verification tools, often, employ theorem proving technology. This technology encompasses an underlying logic encoded in a theorem prover. VDM-LPF, first developed by Sten Agerholm and Jacob Frost in 1996, encodes VDM's Logic of Partial Functions (LPF) by extending the generic theorem prover Isabelle. Because of Isabelle's powerful syntax facilities, terms in this logic are written using a subset of the VDM-SL specification language. In this thesis we provide the reader with a detailed description of the steps we undertake to revive the VDM-LPF logic by upgrading it to the latest Isabelle version, namely Isabelle2005, and by using its latest Intelligible Semi-Automated Reasoning (Isar) theory syntax. We first provide a description of the Isabelle theorem prover, its generic design, and the unique facilities it provides for extending itself and developing new object-logics. We then explain in detail the original VDM-LPF system as developed for the Isabelle94-8. We describe all the necessary modifications that were needed to perform the upgrade. Finally, a number of proofs are performed, using the upgraded VDM-LPF system, that form a case-study.