- Open Proofs
- Java modeling unsound Taclet Options
- Taclet Options with additional Information
- Assumptions
1 of 3 proof is still open:
-
/SWTBotVerificationStatusViewTest_testColorOfCyclicProofs/proofs/cp/MR.java/cp_MR[cp_MR__b()]_JML_normal_behavior_operation_contract_0.proof
Proofs using a listed taclet options are Java modeling unsound:
-
initialisation:disableStaticInitialisation (Java modeling unsound)
-
intRules:arithmeticSemanticsIgnoringOF (Java modeling unsound)
Proofs using a taclet option with some additional information:
-
assertions:on (Sound if JVM is started with enabled assertions for the whole system.)
-
JavaCard:off (Sound if a Java program is proven.)
Proofs are performed under the following assumptions still need to be proven:
-
Closed world assumption for the dynamic dispatch of the following method calls:
-
cp.MR#()
-
cp.MR#()
-
cp.MR#()
-
java.lang.Object#()
-
java.lang.Object#()
- Methods are called in a state satisfying the precondition, assumed for:
- Methods of used APIs
- System in which the source code will be used
- No VirtualMachineError can occur during execution, e.g. OutOfMemoryError or StackOverflowError.
- Threading does not influence sequential execution.
- Garbage collection does not influence program execution.
- The used Java compiler is correct.
- The Java Virtual Machine (JVM) is correct.
- This list is complete.