<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE properties SYSTEM "http://java.sun.com/dtd/properties.dtd">
<properties>
<comment>
  These properties define the help comments which are to be displayed
  in the taclet option dialog
</comment>
<entry key="assertions">Treatment of Java assertion statements

Java assertions can be handled in three different ways in KeY:

* If switched 'off', assert statements are skipped.

* 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 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.
</entry>

<entry key="JavaCard">
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 transac-
tion.
</entry>

<entry key="javaLoopTreatment">
Java loop invariant rules.

* 'efficient': Uses the original loop scope method with two branches.
  
  Recommended for long and complicated loops, especially for real-world
  problems.
  
* 'teaching': Loop Invariant treatment producing the well-known three
  branch structure (base case ('Invariant Initially Valid'), step ('Body
  Preserves Invariant'), Use Case).
  
  Recommended for teaching.

Background:

The loop scope method is an efficient way to apply loop invariants to
loops in Java programs. It does not transform the body of a loop and
handles irregular termination (exceptions, breaks, returns, continues)
gracefully. In its pure variant, the preserved (step) and use case parts
are combined to one single proof branch, which spares duplicate code
execution, but is less easy to comprehend since the traditional three-step
structure frequently used in teaching is not easy to see. Therefore,
there is a loop-scope based loop invariant rule with three branches,
which is less efficient (and thus not recommended for complex and long
real-world programs), but more transparent: If a proof case in the 
preserved branch cannot be closed, one can be sure that it is related to
an invariant that cannot be proven (and not to the post condition), and
vice versa for the use case.
</entry>

<entry key="mergeGenerateIsWeakeningGoal">
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.
</entry>

<entry key="floatRules">
Rules for how to deal with floating point operations.  A JVM
implementation may choose to use a datatype with a higher precision
than float or double.

All KeY rules concerning floating point numbers, as well as their
translation to SMT-LIB, only make sense for strictfp floats where the
semantics is fixed.

* assumeStrictfp: treat all floats as if they came from a class class
annotated strictfp. This is convenient, but not always sound, as the
compiler might make optimizations which break some assumptions which
the KeY rules and SMT-LIB translation depend on.

* strictfpOnly: floats are usable, but they are only translated to the
respective IEEE typed if they come from a class or method annotated
strictfp, and remain uninterpreted functions otherwise.
</entry>

    <entry key="initialisation">
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.
</entry>

<entry key="intRules">
This option controls how integer numbers are modeled.

* '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.

* '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.

* '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.
</entry>

<entry key="programRules">
Rules dealing Java language constructs can be turned off by setting
this to 'None'.
</entry>

<entry key="runtimeExceptions">Treatment of implicit runtime exceptions

* If set to 'allow', implicit runtime exceptions are raised as specified 
  in the Java language specification.

* 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.
</entry>

<entry key="modelFields">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.

* 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.
  
* 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.
</entry>

<entry key="Strings">
Loading rules dealing with Strings (charLists) can be disabled.
</entry>

<entry key="bigint">
Loading program rules dealing with JML's \bigint datatype can be disabled.
</entry>

<entry key="sequences">
Loading rules dealing with sequences can be disabled.
</entry>

<entry key="moreSeqRules">
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. 
</entry>

<entry key="reach">
Loading rules dealing with reachability can be disabled.
</entry>

<entry key="integerSimplificationRules">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.
</entry>

<entry key="optimisedSelectRules">
The optimized select rules can be turned off by setting this option to off.

The unoptimized rules use inplace rewriting for the evaluation of select terms. This may lead to heap terms growing exponentially in the number of anons/stores to be evaluated. However, in some rare cases the usage of the unoptimized rules may lead to more human readable sequents.

The optimized rules pull out select terms before they evaluate them. Because other occurences of the same select term are replaced by the Skolem constant introduced by the pullout rule (application of equalities), each select term has to be evaluated only once. Intelligent hiding of no longer needed auxiliary equations holds the sequent human readable and increases performance. The result of the evaluation of a select term is stored such that it can be reapplied immediately if the same select term occurs again.
</entry>

<entry key="wdOperator">
Treatment of formulas and terms for welldefinedness checks:

* L-Operator:
     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.

* Y-Operator:
     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.

* D-Operator:
     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
</entry>

<entry key="wdChecks">
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.
</entry>
</properties>

