Lecture 13: Practical Tools for Java Correctness

Title slideToday’s lecture presented two different facilities designed to help write Java code that does the right thing: the Java assert statement; and JML, the Java Modeling Language.

Both of these approaches aim to record the programmers’ expectations about what code is doing. The most immediate effect of this is that the programmer has to actually consider and make precise what those expectations are; after that, making them explicit means that others can read, understand, and possibly challenge them. All this can happen without a formal annotation language or machine assistance. However, once we do use a precise language, it becomes possible to automatically check whether a program does meet the given specification.

There are many different routes to such checks. The assert statement in Java tests that running code behaves as expected. The more extensive JML framework uses a Hoare-like annotation language to support many different kinds of check: static checking of properties before compilation; machine-generated test suites; automatic insertion of run-time checks; and more.

In all of these we are expanding the language not to write programs with a wider range of behaviours or effects, but to write programs that have the correct behaviours or effects for the task they are to perform.

Links: Slides for Lecture 13; Recording (screen and audio)

Homework

JML is just one of many frameworks for specifying and verifying code. Other examples include FindBugs™, QuickCheck, the C specification language ACSL and the Frama-C platform, Spec#, and many more. Your homework is to use a small part of one such system.

Read this: Find out about Type Annotations and Pluggable Type Systems by reading the Oracle Java Tutorial lesson with that name.

Do this: Try these out the @NonNull and @Nullable annotations on the Checker Framework live demo: at http://eisop.uwaterloo.ca/live

Optional extra: The Checker Framework provides twenty different checkers for Java source code through pluggable type-checking.

Browse the manual there to see some of the example checkers. Work through one of these tutorials — for these you will need to install the
Checker Framework and use it through Eclipse or another Java IDE.

References

On assertions in Java and ways to use them
Screenshot Oracle Java Technology Network
Programming with Assertions
Oracle language technical note for Java 8 describing what assertions are and illustrating different ways of using them.
Link: Article
Screenshot Assertions or Exceptions?
pempek.net (Grégory Pakosz)
“In other words, exceptions address the robustness of your application while assertions address its correctness.”
Link: Blog post
Proving correctness or incorrectness of TimSort implementations

The following series of posts in early 2015 on the Envisage project blog describes the discovery of errors in the Java and Python default sorting code, and the role played by formal specification and verification.

There’s also a conference paper summarising the technical details.

Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, Reiner Hähnle. OpenJDK’s Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. In Computer Aided Verification: CAV 2015. LNCS 9206, pp.273–289. Springer-Verlag, July 2015.

The TimSort visualisation is from the magnificent sortvis.org site. As well as a blog post all about TimSort, there’s another making the case that static spatial visualisations beat temporal animations for explaining things.

Weave visualisation of TimSort