Treatment of formulas and terms for welldefinedness checks:
More intuitive for software developers and along the lines of runtime assertion semantics. Well-Definedness checks will be stricter using this operator, since the order of terms/formulas matters. It is based on McCarthy logic. Cf. "Are the Logical Foundations of Verifying Compiler Prototypes Matching User Expectations?" by Patrice Chalin.
This is the default option.
Complete and along the lines of classical logic, where the order of terms/formulas is irrelevant. This operator is equivalent to the D-operator, but more efficient. Cf. "Efficient Well-Definedness Checking" by Ádám Darvas, Farhad Mehta, and Arsenii Rudich.
Complete and along the lines of classical logic, where the order of terms/formulas is irrelevant. This operator is not as strict as the L-operator, based on strong Kleene logic. To be used with care, since formulas may blow up exponentially. Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and Jean-Marc Meynadier
Welldefinedness checks of JML specifications can be turned on/off. This includes class invariants, operation contracts, model fields as well as JML (annotation) statements as loop invariants and block contracts. The former ones are checked "on-the-fly", i.e., directly when they are applied in the code while proving an operation contract, since the context is needed.