JML and OpenJML for Java 16
17 Citations•2021•
David R. Cok
journal unavailable
Questions about language definition, joint efforts, and community engagement, some enumerated in this paper, for the Java formal reasoning community to address are raised.
Abstract
As the Java language evolves, the Java Modeling Language (JML) and the OpenJML deductive verification tool must evolve with it. Changes in Java since Java 8 bring language and organizational changes which affect the semantics of JML and the implementation of OpenJML. They also raise questions about language definition, joint efforts, and community engagement, some enumerated in this paper, for the Java formal reasoning community to address.