Treatment of Java assertion statements. Java assertions can be handled in three different ways in KeY.
If set to 'safe', the following proof obligations have to be shown: - The program with assertions removed must fulfill the specification - The asserted conditions must hold (without throwing an exception, and with termination) - The assertions do not have side effects influencing the post conditions. This is the default option. Proofs with this option are typically harder.
This is the default option.
If switched 'on', assertions are treated like Java would treat them: Asserted Statements are evaluated and an AssertionException is raised if they turn out to be false.
If switched 'off', assert statements are skipped.
Specifies whether static (class loading) initialization should be taken in consideration.
Both specifications and proof obligations become significantly more
difficult since class loading may take place at many places.
initialisation : { disableStaticInitialisation , enableStaticInitialisation }defined in: optionsDeclarations.key Line: 36 Offset :4This option is unsound
This option controls how integer numbers are modeled.
intRules : { arithmeticSemanticsIgnoringOF , arithmeticSemanticsCheckingOF , javaSemantics }defined in: optionsDeclarations.key Line: 46 Offset :4'Arithmetic without overflow checking' treats integers as pure mathematical objects. The proof obligations are often easier to discharge. However, the model does not allow the verification of all properties which hold with Java semantics. Moreover, it allows the verification of properties which do not hold on Java's actual semantics. This is the default option.
This is the default option. **This option is unsound**
'Arithmetic with overflow checking' also treats integers as mathematical objects, but ensures that no overflow occurs. While this model also has a completeness gap, it prevents proving incorrect properties.
**This option is incomplete**
'Java semantics' treat integers the same way Java would treat them. The different integer types operate within their respective value ranges. The bitvector arithmetic is modeled in KeY using modulo expressions. This is sound and complete. Proof obligations tend to get more complex with this setting.
Rules dealing Java language constructs can be turned off by setting this to 'None'.
This option is incomplete
Treatment of implicit runtime exceptions
If set to 'allow', implicit runtime exceptions are raised as specified in the Java language specification.
**This option is incomplete**
If set to 'ban', any occurrence of an implicit runtime exception is considered an unrecoverable program failure. For programs which do not raise implicit runtime exceptions, this is usually easier to prove than 'allow'. This is the default option.
If set to 'ignore', it is assumed that no implicit runtime exception occurs. Warning: Reasoning with these rules is unsound.
**This option is unsound**
JavaCard is a dialect of Java designed for the use in SmartCards. It lacks floating point operations and concurrency, but provides stronger object persistence guarantees.
There are two values for this option 'on' and 'off'. Switching
on or off all taclets axiomatising JavaCard specific features like transaction.
Loading rules dealing with Strings (charLists) can be disabled.
This option is incomplete
Rules for model field representation clauses. JML model fields are given a semantics by represents clauses. This switch sets how the rules handle these clauses.
modelFields : { treatAsAxiom , showSatisfiability }defined in: optionsDeclarations.key Line: 112 Offset :4If set to 'showSatisfiability', for every expansion of the represents
clause, it must be shown that the definition is locally
satisfiable. Cross-definition inconsistencies can still be
formulated, however:
//@ represents modelField1 == modelField2; //@ represents modelField2 == modelField1 + 1;
This had been the default option previously, until KeY 2.2.
Loading program rules dealing with JML's \bigint datatype can be disabled.
Loading rules dealing with sequences can be disabled.
This option allows more fine-grained control over rules dealing with sequences. By default, it is disabled because the additional rules are known to have a negative impact on overall performance. Activate this option if your problem is concerned with permutations or information flow.
Loading rules dealing with reachability can be disabled.
Loading less commonly used rules for (mathematical) integers, such as rules for bounded sums and products, modulo, or polynomials, can be disabled. If they are loaded, their application in the strategy can still be controlled as usual.
This option is experimental. Depending of your understanding of 'less common',
you may experience incompleteness. Doing proofs with Java int semantics will not work, definitely.
Not to be confused with intRules, which controls the semantics of the Java type int.
integerSimplificationRules : { full , minimal }defined in: optionsDeclarations.key Line: 149 Offset :4This option is incomplete
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.
Specifies whether a special goal "Joined node is weakening" should be generated as a child of the partner node of a join operation.
For join procedures formally proven correct, this should not be necessary.
Enable this option when you are not sure whether a newly implemented join
procedure is sound. In this case, the generated "is weakening" goals should
only be closable if the concrete join instance is correct.
Method calls in KeY can be either handled by inlining the method body or by applying the method's contract. Inlining a method body is only modularly sound if it is guaranteed that no new method body can override the known implementation.
methodExpansion : { modularOnly , noRestriction }defined in: optionsDeclarations.key Line: 216 Offset :4Inlining is modularly sound: Methods can only be inlined if private, static, final, or in a final method. This is the default option.
Inlining is liberal: Methods can always be inlined, and all known method implementations are taken into consideration. This setting is sound under a closed program assumption.
Missing documentation
Floating points in Java may have a more precise semantics if the hardware supports it. Only if the Java keyword strictfp is specified can we make guarantees about the meaning of floating point expressions.
floatRules : { strictfpOnly , assumeStrictfp }defined in: optionsDeclarations.key Line: 240 Offset :4Require the strictfp keyword if floating points are to be treated. Otherwise arithmetic remains as underspecified symbols
Treat all code as if it was specified strictfp.