Login | Register

A modern Isabelle-based prover for VDM's logic of partial functions


A modern Isabelle-based prover for VDM's logic of partial functions

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)
Authors:Karabotsos, George
Pagination:ix, 158 leaves ; 29 cm.
Institution:Concordia University
Degree Name:M. Comp. Sc.
Program:Computer Science and Software Engineering
Thesis Supervisor(s):Chalin, Patrice
ID Code:8505
Deposited By: Concordia University Libraries
Deposited On:18 Aug 2011 18:27
Last Modified:18 Aug 2011 18:27
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page


Downloads per month over past year

Back to top Back to top