F. What's Missing

What is missing from this reference manual?

The following constructs are not discussed at all:

• abrupt_behavior
• breaks and breaks_redundantly
• choose and choose_if
• continues and continues_redundantly
• example and exceptional_example
• implies_that
• hence_by and hence_by_redundantly
• model_program
• returns and returns_redundantly
• weakly xxx

Other stuff not to forget - DRCok

• \not_specified
• \nothing
• \everything
• nowarn annotation
• methods and constructors without bodies in java files
• methods and constructors with bodies in specification files
• methods and constructors in annotation expressions - purity - modifies clauses - various checking
• anonymous and block-level classes
• field, method, constructor keywords
• exceptions in annotation expressions