Compiler support for learning program invariants

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.