OpenJML Checks
These tables list the various checks that OpenJML performs on a Java program.
Java language checks
JML assertions
JML assumptions
Java Language Checks
These are program errors that would result in Java runtime exceptions.OpenJML Key Java Exception |
Description | Comments |
PossiblyNullValue NullPointerException |
Illegal null value in Java expressions: switch expression, synchronized statement, throw statement | |
PossiblyNullDeReference NullPointerException |
Null dereference in Java expressions: o may not be null in o.f, o.m(), o[i] | |
PossiblyNegativeSize NegativeArraySizeException |
In Java array creation expressions, the size may not be negative | |
PossiblyNegativeIndex ArrayIndexOutOfBoundsException |
In Java array reference expressions, the index may not be negative | |
PossiblyTooLargeIndex ArrayIndexOutOfBoundsException |
In Java array reference expressions, the index must be less than the length of the array | |
PossiblyDivideByZero ArithmeticException |
In Java expressions, checks that a Division or Mod operation has a non-zero divisor | |
PossiblyBadCast ClassCastException |
In Java expressions, checks that the target type of a cast is legitimate | |
PossiblyLargeShift |
In Java shift expressions (a << b , a >> b , a >>> b ), only the lower 5 bits (for 32-bit operations) of the shift value (b ) are used.
That is, a << 32 is equivalent to no shift, not to a shift of all the bits of a 32-bit value. Though values of
b larger than 31 are not illegal, they can be confusing. OpenJML warns if the value of the right-hand-side is greater or equal to the number of bits in the promoted type of the left-hand-side. |
|
PossiblyNullUnbox |
The argument of an unboxing operation must not be null | |
Assert AssertionError |
Explicit Java assert statement | For RAC, the JML check is performed when -racJavaChecks is enabled for rac compilation |
PossiblyBadArrayAssignment ArrayStoreException |
Runtime assignment of an object as an array element, where the runtime class of the object is not a subtype of the dynamic class of the array elements | Implemented for ESC; RAC results in only the Java error |
TBD |
Other possibilities: EmptyStackException, EnumConstantNotPresentException, NoSuchElementException, IndexOutOfBoundsException, StringIndexOutOfBoundsException, UnmodifiableSetException, InputMismatchException, ConcurrentModificationException (when multi-threaded analysis is supported) | Possible |
JML Checks
These are assertions that can be expressed in JML and are checked by OpenJML.OpenJML Key | Description | Comments |
Assert |
Explicit JML assert statement | |
PossiblyNullInitialization |
The initializing expression for a declaration of a variable that is declared NonNull must not be null | |
PossiblyNullAssignment |
The value assigned to a variable or field declared NonNull must not be null | |
Postcondition |
Normal postconditions must be true at non-exceptional termination of a method | |
ExceptionalPostcondition |
Exceptional postconditions must be true when a method ends with an exception | |
ExceptionList |
An expression was thrown whose type is not in the signals_only specification | |
Invariant | Class invariants must be true when a method ends either normally or with an exception | |
InvariantLeaveCaller | Class invariants must be true in the caller when a method is called | |
InvariantEntrance | Class invariants must be true at the beginning of a callee when a method is called | |
InvariantExit | Class invariants must be true at the end of a callee when a method is called | |
InvariantReenterCaller | Class invariants must be true in the caller when a called method returns | |
Assignable |
Assignable clauses must be satisfied at each assignment statement or return from a called method | |
Constraint |
A constraint clause must be true at a normal or exception termination of a method (but not a constructor) | |
Initially |
An initially clause must be at a normal or exceptional termination of a constructor (but not a method) | |
Unreachable |
A JML unreachable statement must be be able to be executed (equivalent to 'assert false') | |
LoopInvariant |
A JML loop invariant must be true at the end of a loop body | |
LoopDecreases |
A JML loop variant value must decrease from the beginning of a loop body to the end of the loop body | |
LoopDecreasesNotPositive |
A JML loop variant value must be zero or positive at the beginning of a loop, at the beginning of each loop body, and when the loop condition tests false (but not necessarily on a break from the loop) | |
UndefinedCalledMethodPrecondition |
Calling a method whose composite precondition is not true is not allowed in a JML expression. The composite precondition is the disjunction of all relevant (visible and normal???) specification cases. |
Undefined JML expressions
JML expressions are not allowed to exit with exceptions; an expression that does is undefined.OpenJML Key Java Exception |
Description | Comments |
UndefinedNullReference NullPointerException |
Null dereference in JML expressions: o may not be null in o.f, o.m(), o[i] | |
UndefinedNegativeSize NegativeArraySizeException |
In JML array creation expressions, the size may not be negative | |
UndefinedNegativeIndex ArrayIndexOutOfBoundsException |
In JML array reference expressions, the index may not be negative | |
UndefinedTooLargeIndex ArrayIndexOutOfBoundsException |
In JML array reference expressions, the index must be less than the length of the array | |
UndefinedDivideByZero ArithmeticException |
Division or Mod operations with a divisor of zero are not permitted in JML expressions | |
UndefinedBadCast ClassCastException |
A cast to an illegal type is not allowed in a JML expression |
JML Assumptions
These are assumptions that are explicit or implied by JML and are inserted into the program by OpenJML. Runtime-assertion compilation can be configured to check these assumptions as assertions.OpenJML Key | Description | Comments |
Assume |
Explicit JML assume statement | |
Axiom |
Axioms declared in classes are assumed to be true at the beginning of a method (and assumed to be always true, though not subsequently checked) | |
DSA |
Assumptions (assignments) introduced to implement Dynamic Static Assignment | |
Precondition |
At the beginning of a method, it is assumed that at least one precondition is true | |
LoopInvariantAssumption |
A JML loop invariant is assumed to be true at the beginning of a loop body | |
TBD | Exceptional postconditions must be true when a method ends with an exception | |
TBD | Exceptional postconditions must be true when a method ends with an exception |
Last modified MODDATE.