Report

List of Contents

  1. Unspecified Methods
  2. Taclet Options with additional Information
  3. Assumptions

Unspecified Methods

1 of 2 method is unspecified and may call methods in a state not satisfying the precondition:
  1. Magic

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. Methods are called in a state satisfying the precondition, assumed for:
    1. Unspecified methods
    2. Methods of used APIs
    3. System in which the source code will be used
  2. No VirtualMachineError can occur during execution, e.g. OutOfMemoryError or StackOverflowError.
  3. Threading does not influence sequential execution.
  4. Garbage collection does not influence program execution.
  5. The used Java compiler is correct.
  6. The Java Virtual Machine (JVM) is correct.
  7. This list is complete.