| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
20.1 Deprecated Syntax 20.2 Replaced 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.
20.1.1 Deprecated Represents Clause Syntax 20.1.2 Deprecated File Name Suffixes
The following syntax for a functional represents-clause is deprecated.
represents-clause ::= represents-keyword store-ref-expression |
Instead of using the <-, one should use = in such a
represents-clause.
See section 8.4 Represents Clauses, for the supported syntax.
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 16.1 File Name Suffixes, for details on the use of file names with JML tools.
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.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |