OpenJML (JML)

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.

NullCheck NullField ExceptionList MethodAxiom AssumeCheck arithmetic checks

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

ImplicitAssume ArgumentValue Assignment ReceiverValue BlockEquation BranchCondition BranchThen BranchElse Case Havoc Invariant InvariantReenterCaller InvariantEntrance InvariantExit InvariantLeaveCaller CatchCondition SwitchValue ArrayInit Lbl Return Termination Synthetic LoopInvariantBeforeLoop LoopInvariantAfterLoop LoopCondition

Last modified MODDATE.