#102 Typecheck level 0 JML statements

[Curtis Clifton]

All of the Java statements and most of the JML extensions for adding assertions to statements and annotation statements (see section 12. Statements and Annotation Statements) are at level 0. But redundancy features of the JML extensions are only present at level 1, not at level 0. We describe the level 0 extension to statements below.

Using the modifier ghost in local-declarations (see section 12.1.1 Modifiers for Local Declarations).
The possibly-annotated-loop statement (see section 12.2 Loop Statements), with a loop-invariant (see section 12.2.1 Loop Invariants). The redundant forms of loop-invariants, namely those that use the keywords maintaining_redundantly and loop_invariant_redundantly are level 1 features. Furthermore, the variant-function is a level 1 feature.
The assert-statement (see section 12.3 Assert Statements). Note that the assert-redundantly-statement, which uses the keyword assert_redundantly, is in level 1.
The non-redundant form of the assume-statement (see section 12.4.1 Assume Statements). Use of the keyword assume_redundantly is a level 1 feature.
The set-statement (see section 12.4.2 Set Statements).