01whole.pdf (11.84 MB)
Download file

Dafny-style verification of MiniJava programs

Download (11.84 MB)
thesis
posted on 28.03.2022, 14:31 by Joseph Bell
Software verification is the process of proving that a program fulfils all of its expected requirements. It is a crucial component of software engineering and is vital for successful software. This project is in the area of software verification and attempts to create a Dafny style verification system for the MiniJava language. The system is part of a MiniJava compiler so programs can be verified at compile time. t contains the basic features of the Dafny programming language, a language with inbuilt specification constructs, as well as some of its more advanced ones if time permits. The verification specifications are defined by the programmer as part of the MiniJava source code. Any verification errors are displayed to the user. The project research will build such a system and determine whether or not every desire verification feature can be recreated in MiniJava. The project is focused specifically around the MiniJava language as a MiniJava compiler is available for use in the project and MiniJava is a very basic language with a limited feature set. These two aspects allow for the task to be feasible for a project of this scale.

History

Table of Contents

1. Introduction -- 2. Literature review -- 3. Background : Hoare logic -- 4. Design -- 5. Implementation -- 6. Discussion -- 7. Conclusions -- 8. Future work -- Appendices.

Notes

Bibliography: pages 63-64 Empirical thesis.

Awarding Institution

Macquarie University

Degree Type

Thesis bachelor honours

Degree

BSc (Hons), Macquarie University, Faculty of Science and Engineering, School of Engineering

Department, Centre or School

School of Engineering

Year of Award

2016

Principal Supervisor

Anthony Sloane

Rights

Copyright Joseph Bell 2016. Copyright disclaimer: http://mq.edu.au/library/copyright

Language

English

Extent

1 online resource (xiii, 64 pages tables)

Former Identifiers

mq:70335 http://hdl.handle.net/1959.14/1262673

Usage metrics

Keywords

Exports