Formal Methods for Components and Object (FMCO) 2005

Beyond Hoare Logic Assertions: Advanced Specification and Verification with JML and ESC/Java2

JML is a large, rich specification language---some would say too rich.

In our tutorials we have covered the "basics" of JML, Hoare logic assertions, invariants, etc. In this talk we focus on those "advanced" constructs of JML that we find most useful in writing specifications for non-trivial Java programs. These constructs include data groups, model fields and methods, etc.

This talk included a walk through select specifications from the JavaCard API and the Java API. We also demonstrated ESC/Java2 summarised some of the ongoing research on extended static checking.

A follow-up journal article that covers this materials in detail will be available soon.