Description

To specify and verify the behaviour of a Java program, JML (the Java Modelling Language) is often used to specify the program. There exist two well-established tools to verify such JML annotations. KeY works more interactively, while verification with OpenJML is fully automatic (provided the right annotations are given).

However, the tools implement slightly different variations of JML, and a good understanding of these differences is needed.

Goal of this project is to take several Java programs annotated with JML, and verified with KeY, and to understand how the specifications need to be adapted to be verifiable with OpenJML. These changes can range from syntactical changes (slightly different keywords), to problems related to visiblity and semantical differences.

The question that should be investigate is: how big are the differences, which changes could be made to unify the specification languages understood by the different tools, and where are real differences in what can be verified with one tool and not with the other one.

If time permits, the exercise also could be done the other way round, i.e., take an example program verified with OpenJML and check if this can be verified with KeY as well.

The developers of KeY and OpenJML will be happy to help with the supervision of the project, and are very interested in the results.