Diploma Thesis:
A Proof Obligation Generator for the IFAD VDM-SL Toolbox

Author(s): Aichernig, Bernhard

Written in: English

Keywords:
Software engineering; Vienna Development Method - Specification Language (VDM-SL); formal methods; static semantics

Abstract:
This thesis describes an extension of the IFAD VDM-SL Toolbox, a CASE tool supporting the formal method VDM (Vienna Development Method). Amongst other features the Toolbox provides parsing and type checking of specifications written in VDM-SL, the specification language of VDM. Static type checking in VDM-SL is undecidable in general and therefore the type checker must be in- complete. In traditional programming languages the additional consistency checks are performed at run time. This approach is not feasible, because speci- fications are not executable in general. Hence, it is up to the user to verify the consistency of a specification for the "difficult" parts introducing un- decidability. In the existing type checker the user is supported by error messages and warnings generated during type checking. Instead of providing error messages, here the approach of generating proof obligations (PO) for consistency is described. A PO is an unproved theorem stating that a certain property must hold in order for the specification to be consistent. If a PO can be proved, then the referred part in the specification is consistent. The goal of the thesis project was the specification of a PO generator in VDM- SL as an extension to the existing static semantics of the Toolbox. The POs are designed to be imported into a proof tool for the Toolbox which is under development.

Advisor(s):
Lucas, Peter; Gorm Larsen, Peter

TECHNICAL UNIVERSITY GRAZ, Institut für Informationsverarbeitung und Computergestützte Neue Medien
Degree Course: 874 / Telematik