Treatment of Java assertion statements. Java assertions can be handled in three different ways in KeY.
/*!
Treatment of Java assertion statements. Java assertions can be handled in three different ways in KeY.
*/ assertions : { /*!
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.
@choiceDefaultOption
*/ safe , /*! 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.*/ on , /*! If switched 'off', assert statements are skipped. */ off } defined in: optionsDeclarations.key Line: 11 Offset :4If 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.
/*! 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 : { /*! @choiceUnsound */ disableStaticInitialisation , enableStaticInitialisation } defined in: optionsDeclarations.key Line: 36 Offset :4This option is unsound
This option controls how integer numbers are modeled.
/*! This option controls how integer numbers are modeled. */ intRules : { /*! '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.
@choiceDefaultOption @choiceUnsound
*/ arithmeticSemanticsIgnoringOF , /*! '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.
@choiceIncomplete*/ arithmeticSemanticsCheckingOF , /*! '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.*/ 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'.
/*! Rules dealing Java language constructs can be turned off by setting this to 'None'. */ programRules : { Java , /*! @choiceIncomplete */ None } defined in: optionsDeclarations.key Line: 75 Offset :4This option is incomplete
Treatment of implicit runtime exceptions
/*! Treatment of implicit runtime exceptions */ runtimeExceptions : { /*! If set to 'allow', implicit runtime exceptions are raised as specified
in the Java language specification.
@choiceIncomplete
*/ ban , /*!
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.
*/ allow , /*! If set to 'ignore', it is assumed that no implicit runtime exception occurs.
Warning: Reasoning with these rules is unsound.
@choiceUnsound
*/ ignore } defined in: optionsDeclarations.key Line: 77 Offset :4If 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.
/*! 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.
*/ JavaCard : { off , on } defined in: optionsDeclarations.key Line: 100 Offset :4Loading rules dealing with Strings (charLists) can be disabled.
/*! Loading rules dealing with Strings (charLists) can be disabled. */ Strings : { on , /*! @choiceIncomplete */ off } defined in: optionsDeclarations.key Line: 109 Offset :4This 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.
/*!
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 : { /*!
* If set to 'treatAsAxiom', the representation is seen as an axiom,
satisfiability will not be checked. This may introduce inconsistent
specifications, for example the following contradictory JML clause
will not be rejected:
//@ represents modelField == modelField + 1;
This is the default option since KeY 2.4.
*/ treatAsAxiom , /*!
If 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.
*/ 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 program rules dealing with JML's \bigint datatype can be disabled. */ bigint : { on , off } defined in: optionsDeclarations.key Line: 139 Offset :4Loading rules dealing with sequences can be disabled.
/*! Loading rules dealing with sequences can be disabled. */ sequences : { on , off } defined in: optionsDeclarations.key Line: 141 Offset :4This 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.
/*! 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.*/ moreSeqRules : { off , on } defined in: optionsDeclarations.key Line: 143 Offset :4Loading rules dealing with reachability can be disabled.
/*! Loading rules dealing with reachability can be disabled. */ reach : { on , off } defined in: optionsDeclarations.key Line: 147 Offset :4Loading 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.
/*!
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 , /*! @choiceIncomplete */ minimal } defined in: optionsDeclarations.key Line: 149 Offset :4This option is incomplete
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.
/*!
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.
*/ mergeGenerateIsWeakeningGoal : { off , on } defined in: optionsDeclarations.key Line: 164 Offset :4Method 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.
/*!
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 : { /*! Inlining is modularly sound: Methods can only be inlined if private,
static, final, or in a final method.
@choiceDefaultOption
*/ modularOnly , /*! 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.
*/ noRestriction } defined in: optionsDeclarations.key Line: 175 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.
Final fields can only be written to from within the constructor. This is a Java language feature. KeY can exploit this restriction by treating final fields as immutable. This can simplify the reasoning about the program significantly. But it is still possible to tread final fields as normal mutable fields to ensure backward compatibility. If constructor code is to be inlined, there can be cases where the immutable treatment is incomplete.
/*!
Final fields can only be written to from within the constructor. This is a
Java language feature. KeY can exploit this restriction by treating final fields
as immutable. This can simplify the reasoning about the program significantly.
But it is still possible to tread final fields as normal mutable fields to
ensure backward compatibility. If constructor code is to be inlined, there
can be cases where the immutable treatment is incomplete.
*/ finalFields : { /*! Final fields are treated as immutable entities.
This is the default option. */ immutable , /*! Final fields are treated like all Java fields.
This is the original behaviour of KeY. */ onHeap } defined in: optionsDeclarations.key Line: 194 Offset :4Final fields are treated as immutable entities. This is the default option.
Final fields are treated like all Java fields. This is the original behaviour of KeY.
Missing documentation
/*!
Missing documentation
*/ javaLoopTreatment : { efficient , teaching } defined in: optionsDeclarations.key Line: 212 Offset :4Floating 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.
/*!
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 : { /*! Require the strictfp keyword if floating points are to be treated.
Otherwise arithmetic remains as underspecified symbols*/ strictfpOnly , /*! Treat all code as if it was specified strictfp. */ assumeStrictfp } defined in: optionsDeclarations.key Line: 217 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.