Karabotsos, George (2005) A modern Isabelle-based prover for VDM's logic of partial functions. Masters thesis, Concordia University.
|PDF - Accepted Version|
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.
|Divisions:||Concordia University > Faculty of Engineering and Computer Science > Computer Science and Software Engineering|
|Item Type:||Thesis (Masters)|
|Pagination:||ix, 158 leaves ; 29 cm.|
|Degree Name:||M. Comp. Sc.|
|Program:||Computer Science and Software Engineering|
|Thesis Supervisor(s):||Chalin, Patrice|
|Deposited By:||Concordia University Libraries|
|Deposited On:||18 Aug 2011 14:27|
|Last Modified:||18 Aug 2011 14:27|
Repository Staff Only: item control page