A. Deprecated and Replaced Syntax

The subsections below briefly describe the deprecated and replaced features of JML. A feature is deprecated if it is supported in the current release, but slated to be removed from a subsequent release. Such features should not be used.

A feature that was formerly deprecated is replaced if it has been removed from JML in favor of some other feature or features. While we do not describe all replaced syntax in this appendix, we do mention a few of the more interesting or important features that were replaced, especially those discussed in earlier papers on JML.

A.1 Deprecated Syntax
A.2 Replaced Syntax

A.1 Deprecated Syntax

The following syntax is deprecated. Note that it might be supported with a deprecation warning by some tools (e.g., JML2) but not by newer tools.

A.1.1 Deprecated Annotation Markers
A.1.2 Deprecated Represents Clause Syntax
A.1.3 Deprecated Monitors For Clause Syntax
A.1.4 Deprecated File Name Suffixes
A.1.5 Deprecated Refine Prefix

A.1.1 Deprecated Annotation Markers

The following lexical syntax for annotation markers is deprecated.

annotation-marker ::= //+@ [ @ ] ... | /*+@ [ @ ] ... | //-@ [ @ ] ... | /*-@ [ @ ] ...

A.1.2 Deprecated Represents Clause Syntax

The following syntax for a functional represents-clause is deprecated.

represents-clause ::= represents-keyword store-ref-expression <- spec-expression ;

Instead of using the <-, one should use = in such a represents-clause. See section 8.4 Represents Clauses, for the supported syntax.

A.1.3 Deprecated Monitors For Clause Syntax

The following syntax for the monitors-for-clause is deprecated.

monitors-for-clause ::= monitors_for ident <- spec-expression-list ;

Instead of using the <-, one should use = in such a monitors-for-clause. See section 8.9 Monitors For Clause, for the supported syntax.

A.1.4 Deprecated File Name Suffixes

The set of file name suffixes supported by JML tools is being simplified. In the future, especially in new tools the suffixes The suffixes `.refines-java', `.refines-spec', `.refines-jml', `.spec', `.java-refined', `.spec-refined', and `.jml-refined' are no longer supported. Instead, one should write specifications into files with the suffixes `.java' and `.jml'. See section 17.1 File Name Suffixes, for details on the use of file names with JML tools.

A.1.5 Deprecated Refine Prefix

The following syntax involving the refine-prefix is deprecated.

compilation-unit ::= [ package-declaration ] refine-prefix [ import-declaration ] ... [ top-level-declaration ] ... refine-prefix ::= refine-keyword string-literal ; refine-keyword ::= refine | refines

Instead of using the refine-prefix in a compilation unit, modern JML tools just use a .jml file that contains any specifications not in the .java file. See section 17. Separate Files for Specifications, for details.

A.2 Replaced Syntax

The +-style of JML annotations, that is, JML annotations beginning with //+@ or /*+@, is being replaced by the annotation-key feature described in See section 4.4 Annotation Markers.

As a note for readers of older papers, the keyword subclassing_contract was replaced with code_contract, which is now removed. Instead, one should use a heavyweight specification case with the keyword code just before the behavior keyword, and a precondition of \same.

Similarly, the depends clause has been replaced by the mechanism of data groups and the in and maps clauses of variable declarations.