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
Assert AssertionError	Explicit Java assert statement	For RAC, the JML check is performed when -ea is enabled at runtime
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
PossiblyBadCast ClassCastException	In Java expressions, checks that the target type of a cast is legitimate
PossiblyDivideByZero ArithmeticException	In Java expressions, checks that a Division or Mod operation has a non-zero divisor
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
PossiblyNullUnbox NullPointerException	A value being unboxed must not be null
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]
PossiblyTooLargeIndex ArrayIndexOutOfBoundsException	In Java array reference expressions, the index must be less than the length of the array
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.
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. log-release-tests 5

OpenJML Key	Description	Comments
Accessible	Violation of an accessible clause
ArithmeticCastRange	An arithmetic cast causes loss in precision, in safe math mode
ArithmeticOperationRange	An arithmetic operation results in an out-of-range value, in safe math mode
Assert	Explicit JML assert statement
Assignable	Assignable clauses must be satisfied at each assignment statement or return from a called method
Callable	A callable clause must be satisfied
CompletePreconditions	The preconditions of a method must cover all possible cases
Constraint	A constraint clause must be true at a normal or exception termination of a method (but not a constructor)
DisjointPreconditions	The preconditions of a method must be pairwise disjoint
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
IllegalArgument	An argument of a JML expression is illegal
Initially	An initially clause must be at a normal or exceptional termination of a constructor (but not a method)
Invariant	Class invariants must be true when a method ends either normally or with an exception
InvariantEntrance	Class invariants must be true at the beginning of a callee when a method is called
InvariantExceptionExit	Class invariants must be true in exception exits of a method
InvariantExit	Class invariants must be true at the end of a method
PossiblyLargeShift NullPointerException	The shift amount in a left shift operation is legative or larger than the number of bits in the lhs type
LoopDecreases	A JML loop variant value must decrease from the beginning of a loop body to the end of the loop body
LoopDecreasesNonNegative	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)
LoopInvariant	A JML loop invariant must be true at the end of a loop body
LoopInvariantAfterLoop	A JML loop invariant must be true at a normal exit of a loop
LoopInvariantBeforeLoop	A JML loop invariant must be true before the loop is started
NullArgument	An argument is null where non-null is required
NullField	A non-null field is assigned a null value
NullFormal	An argument is null where non-null is required
PossiblyNullAssignment	The value assigned to a variable or field declared NonNull must not be null
PossiblyNullDereference	The receiver expression in a dot-dereference must not be null`
PossiblyNullInitialization	The initializing expression for a declaration of a variable that is declared NonNull must not be null
PossiblyNullReturn	The return value from a method is null where it is expected to be non-null
Postcondition	Normal postconditions must be true at non-exceptional termination of a method
Precondition	The precondition of a called method must be true
Reachable	A JML reachable statement must be be able to be executed	Only checked with --check-feasibility
Readable-if	A JML readable clause must be true when the corresponding field is read
StaticInit	Static invariants and non-nullness of static fields must hold at the end of static initialization
TerminationDecreases	A termination metric must decrease on recursive calls
TerminationNonNegative	A termination metric must not become negative
Unreachable	A JML unreachable statement must not be able to be executed (equivalent to 'assert false')
UndefinedPrecondition	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.
Writable-if	A JML writable clause must be true when the corresponding field is assigned

MethodAxiom AssumeCheck

Undefined JML expressions

JML expressions must be well-defined, which includes not exiting with exceptions.

OpenJML Key Java Exception	Description	Comments
Choose	A \choose expression is undefined
ChooseX	A \choosex expression is undefined
UndefinedBadCast ClassCastException	An illegal reference casst, within a JML expression
UndefinedBigintUSR	The argument of an unsigned right-shift of a bigint value must be non-negative
UndefinedLemmaPrecondition	The precondition of a lemma call in a 'use' statement must be true
UndefinedNegativeIndex ArrayIndexOutOfBoundsException	In JML array reference expressions, the index may not be negative
UndefinedNegativeSize NegativeArraySizeException	In JML array creation expressions, the size may not be negative
UndefinedNullReference NullPointerException	Null dereference in JML expressions: o may not be null in o.f, o.m(), o[i]
UndefinedNullUnbox NullPointerException	In a JML expression, an unboxing operation must have a non-null argument
UndefinedNullValue NullPointerException	In a JML expression, a switchx expression must have a non-null argument
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)
InvariantEntranceAssumed	An invariant is assumed to be true at the beginning of a called method
InvariantExitAssumed	An invariant is assumed to be true by the caller after exit from a called method
LoopInvariantAssumption	A loop invariant is assumed to be true at the beginning of a loop body
NullField	A non-null field must have a non-null value if checked by RAC
Precondition	At the beginning of a method, it is assumed that at least one precondition is true
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 Synthetic LoopCondition

Last modified MODDATE.