G. Differences

The subsections below detail the differences between the JML Common Tools release of JML and other tools and between JML and Java itself.

G.1 Differences Between JML and Other Tools
G.2 Differences Between JML and Java

G.1 Differences Between JML and Other Tools

ESC/Java [Leino-Nelson-Saxe00] and JML share a common syntax; this is even more true of ESC/Java2 and JML. The initial efforts to merge syntaxes were due to the efforts of Raymie Stata. After a long process, the syntax of ESC/Java and JML were both changed and JML was nearly a superset of ESC/Java when work on ESC/Java stopped with ESC/Java 1.2.4. Following the open-source release of ESC/Java, Kiniry and Cok began work on ESC/Java2, which is now very compatible with JML's syntax [Kiniry-Cok04]. Users can thus use both tools with little or no changes to their files.

Similarly the Daikon tool [Ernst-etal01] also uses a variant of JML's syntax, as do several other tools [Burdy-etal03]. While efforts are ongoing to avoid differences, some differences are unavoidable, as research is ongoing (and people have other things to do).

We discuss the differences between the JML language described in this manual and the variants used in these other tools below.

G.1.1 Differences Between JML and ESC/Java2

G.1.1 Differences Between JML and ESC/Java2

This section discusses the current state of affairs of ESC/Java2 compatibility with JML's syntax.

The following differences remain between ESC/Java2 and JML.

• ESC/Java2 is tolerant (with a suppressible warning) of missing semicolons at the ends of annotations, in many circumstances.

• ESC/Java2 does not enforce the visibility modifiers.

• ESC/Java2 strictly requires whole syntactic constructs within a single annotation comment; JML tools are more lenient.

• JML and ESC/Java2 differ in the search order for refinement files in the classpath.

• JML and ESC/Java2 differ in where helper annotations are permitted.

• JML does not support model classes (at least in runtime assertion checking).

• ESC/Java2 reads but ignores model programs.

The following differences between ESC/Java2 and JML are designed to remain differences. While the plan is for ESC/Java2 to parse all of JML's syntax, there are times when one needs to write annotations for one of these tool that are not understood by the other. Thus these differences are intended to allow users of both tools to write such annotations.

• JML supports annotation forms //+@ and /*+@ ... @+*/, so that annotations that JML understands but ESC/Java doesn't can be written.

• ESC/Java2 supports annotation forms //-@ and /*-@ ... @-*/, so that annotations that ESC/Java2 understands but JML doesn't can be written.

G.2 Differences Between JML and Java

This section describes differences between JML and Java without JML. Currently the major differences are the way that JML treats null.

G.2.1 Non-null by Default

G.2.1 Non-null by Default

As described earlier (see section 2.8 Null is Not the Default), JML does not, by default, allow null to be a value in a field, formal parameter, method or a bound variable (see section 12.4.24.5 Modifiers for Bound Variables). To allow null as a value, one has to use the nullable modifier on the declaration, or the nullable_by_default modifier on the type where the declaration occurs See section 6.2.13 Nullity Modifiers, for more details.