Macquarie University
01whole.pdf (11.84 MB)

Dafny-style verification of MiniJava programs

Download (11.84 MB)
posted on 2022-03-28, 14:31 authored 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.


Table of Contents

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


Bibliography: pages 63-64 Empirical thesis.

Awarding Institution

Macquarie University

Degree Type

Thesis bachelor honours


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

Department, Centre or School

School of Engineering

Year of Award


Principal Supervisor

Anthony Sloane


Copyright Joseph Bell 2016. Copyright disclaimer:




1 online resource (xiii, 64 pages tables)

Former Identifiers


Usage metrics

    Macquarie University Theses