[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

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.

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.


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.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html