Report

List of Contents

  1. Open Proofs
  2. Java modeling unsound Taclet Options
  3. Taclet Options with additional Information
  4. Assumptions

Open Proofs

2 of 3 proofs are still open:
  1. /SWTBotVerificationStatusViewTest_testColorOfCyclicProofs/proofs/cp/MR.java/cp_MR[cp_MR__a()]_JML_normal_behavior_operation_contract_0.proof
  2. /SWTBotVerificationStatusViewTest_testColorOfCyclicProofs/proofs/cp/MR.java/cp_MR[cp_MR__b()]_JML_normal_behavior_operation_contract_0.proof

Java modeling unsound Taclet Options

Proofs using a listed taclet options are Java modeling unsound:
  1. initialisation:disableStaticInitialisation (Java modeling unsound)
  2. intRules:arithmeticSemanticsIgnoringOF (Java modeling unsound)

Taclet Options with additional Information

Proofs using a taclet option with some additional information:
  1. assertions:on (Sound if JVM is started with enabled assertions for the whole system.)
  2. JavaCard:off (Sound if a Java program is proven.)

Assumptions

Proofs are performed under the following assumptions still need to be proven:
  1. Closed world assumption for the dynamic dispatch of the following method calls:
    1. cp.MR#()
    2. cp.MR#()
    3. cp.MR#()
    4. java.lang.Object#()
    5. java.lang.Object#()
  2. Methods are called in a state satisfying the precondition, assumed for:
    1. Methods of used APIs
    2. System in which the source code will be used
  3. No VirtualMachineError can occur during execution, e.g. OutOfMemoryError or StackOverflowError.
  4. Threading does not influence sequential execution.
  5. Garbage collection does not influence program execution.
  6. The used Java compiler is correct.
  7. The Java Virtual Machine (JVM) is correct.
  8. This list is complete.