Macquarie University
01whole.pdf (7.8 MB)

Compiler support for learning program invariants

Download (7.8 MB)
posted on 2023-04-19, 06:12 authored by Michael Lay

Formal methods are a skill in high demand for programmers in safety-critical industries. However, the teaching and learning of formal methods is not well understood. We perform a controlled trial of two possible approaches to teaching one fundamental skill from formal methods, and analyse the differences in effectiveness. The fundamental skill is the understanding and creation of program invariants. We compare the traditional method of teaching invariants, which we determined by extensive survey, to a compiler-supported technique. We find no conclusive evidence of a difference in learning speed or depth, however, we do find indications that compiler support is valuable for learners. We provide an in-depth analysis of our data and all material required to build on it. The results indicate a need for larger trials.


Table of Contents

1. Introduction -- 2. Literature Review -- 3. Methods -- 4. Participant Recruitment -- 5. Workshop -- 6. Participant Analysis -- 7. Results -- 8. Discussion -- 9. Conclusion -- Appendices

Awarding Institution

Macquarie University

Degree Type

Thesis MRes

Department, Centre or School

School of Computing

Year of Award


Principal Supervisor

Matthew Roberts

Additional Supervisor 1

Matt Bower


Copyright: The Author Copyright disclaimer:




125 pages

Usage metrics

    Macquarie University Theses