Search

Java code can be annotated with formal specifications using the Java Modelling Language (JML). Previous work has provided IDE plugins intended to help write JML, but mostly for the Eclipse IDE. We introduce IntelliJML, a JML plugin for IntelliJ IDEA, with a focus on ease of use and maintainability. Features such as syntax, semantic, and type checking, as well as syntax highlighting and code completion are integrated into the plugin. The plugin can also be extended in the future to add more features. The source code for the plugin can be found at https://gitlab.utwente.nl/fmt/intellijml.

Modern software relies on libraries and uses them via application programming interfaces (APIs). Correct API usage as well as many software engineering tasks are enabled when APIs have formal specifications. In this work, we analyze the implementation of each method in an API to infer a formal postcondition. Conventional wisdom is that, if one has preconditions, then one can use the strongest postcondition predicate transformer (SP) to infer postconditions. However, SP yields postconditions that are exponentially large, which makes them difficult to use, either by humans or by tools. Our key idea is an algorithm that converts such exponentially large specifications into a form that is more concise and thus more usable. This is done by leveraging the structure of the specifications that result from the use of SP. We applied our technique to infer postconditions for over 2,300 methods in seven popular Java libraries. Our technique was able to infer specifications for 75.7% of these methods, each of which was verified using an Extended Static Checker. We also found that 84.6% of resulting specifications were less than 1/4 page (20 lines) in length. Our technique was able to reduce the length of SMT proofs needed for verifying implementations by 76.7% and reduced prover execution time by 26.7%.

Mungo is an object-oriented language that uses typestates with a behavioural type system to ensure the absence of null-dereferencing. Typestates are usages that specify the admissible sequences of method calls on objects. Previous type systems for Mungo have all had a linearity constraint on objects. We present an extension of these systems, where usage specifications can now include a parallel construct that lets us describe separate local behaviour. A parallel usage describes a separation of the heap, and this allows us to reason about aliasing and to express arbitrary interleaving of local protocols. This also solves the state-space explosion problem for usages. Our extension retains the safety properties of previous type systems for Mungo.