D.1 Deprecated Syntax

The following syntax is deprecated. (Note that incompatible changes and syntax that is no longer supported is not included in this list.)

req-frame-ens ::= [ requires-clause ] [ assuming-clause ] [ frame ] ensures-clause
assuming-clause ::= assuming pre-cond ;

spec-case ::= [ let-clause ] req-frame-ens [ example-seq ] [ claims-seq ]
        | [ let-clause ] [ requires-clause ] [ assuming-clause ] { spec-case-seq }  [ example-seq ] [ claims-seq ]
claims-seq ::= claims-clause [ claims-clause ] ...
claims-clause ::= claims [ liberally ] predicate ;

To update your specifications: change assuming to requires redundantly, move each claims-seq to just after the existing ensures-clause in the same spec-case and change claims to ensures redundantly and move them to before any examples in the same spec-case.

The \ident{X} of identifier, the pure virtual function-specifier, the use of multiple spec-cases without also, and the use of informal-descs for a trait, which were previously deprecated, and have now been removed. If you still have these in your specifications, use ident(X) instead of \ident{X}, add the keyword also between spec-cases, and use the C++ = 0 instead of pure virtual. If you have uses informally in your code, change that to the use of a trait. To specify a trait for a class, struct, or union and prevent Larch/C++ from automatically constructing a trait for it, you need to just specify a signature for some trait function that takes or returns the name of the class, struct, or union. It is often enough just to write the following, for a type T.

uses NoContainedObjects(T)

Go to the first, previous, next, last section, table of contents.