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.

Valid

XHTML 1.0

CSS2