| [ << ] | [ >> ] | [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.
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] | [ ? ] |