The Java Modelling Language (JML) has been proposed as a language that can be used to specify the behavioural details of Java programs. While JML annotations are used in some tools, deductive verifiers (for Java) are still very much developing and adding new types of specifications or ways to express things. As a result, many deductive verifiers for Java have a language that is based on, but slightly different, than JML. This makes it difficult to reuse specifications which is unfortunate since writing specifications is one of the bottlenecks in applying deductive verification in practice.
To alleviate this problem we have developed the Specification Translator. A tool that can translate JML-like specifications while taking into account the semantics of the specification languages. It currently supports Krakatoa, OpenJML and VerCors.
Useful links
- Paper: Lukas Armborst, Sophie Lathouwers and Marieke Huisman. 2024. Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation. In Proceedings of the 18th International Conference on Integrated Formal Methods (IFM 2023). Lecture Notes in Computer Science, vol 14300. Springer, Cham. https://doi.org/10.1007/978-3-031-47705-8_9
- Artefact: https://doi.org/10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f