- Forward


Assertions in Java
An Introduction


Prof. David Bernstein
James Madison University

Computer Science Department
bernstdh@jmu.edu

Print

Motivation
Back SMYC Forward
  • A Common Practice:
    • Include comments in a program that list the assumptions being made
  • The Shortcoming:
    • The programmer must verify that the assumptions hold
  • An Alternative Approach:
    • Include an if statement (e.g., that throws an exception) if the assumption doesn't hold
  • The Shortcoming:
    • This code should be removed before the code is deployed (i.e., it is used for verification not validation)
Overview
Back SMYC Forward
  • Purpose of Assertions:
    • Enable the testing of assumptions while the product is being developed but not after it is deployed
  • Value of Assertions:
    • Help identify faults before the code is deployed
    • Help document code
Syntax
Back SMYC Forward
  • Simple Form:
    • assert boolean_expression;
  • General Form:
    • assert boolean_expression : expression;
Behavior of Assertions
Back SMYC Forward
  • Simple Form:
    • If boolean_expression evaluates to false then an AssertionError is thrown without a detail message
  • General Form:
    • If boolean_expression evaluates to false then an AssertionError is thrown with a String representation of expression as the detail message
Enabling and Disabling Assertions
Back SMYC Forward
  • By Default:
    • Assertions are disabled
  • Enabling/Disabling at Run-Time:
    • Use the -enableassertions (or -ea) switch to enable and/or the -disableassertions (or -da) switch to disable
  • Granularity:
    • No arguments - all classes except system classes
    • ClassName - the named class
    • PackageName - the named package and subpackages
    • ... - The unnamed package in the current working directory
Uses
Back SMYC Forward
  • Appropriate:
    • Internal invariants
    • Control-flow invariants
    • Pre/Post-conditions for private methods
    • Class invariants
  • Inappropriate:
    • Argument checking in public methods (because that is part of the contract of a method)
    • Tasks that are required for correct operation (because assertions may be disabled)
An Example of an Internal Invariant
Back SMYC Forward

This fragment assumes i is non-negative.

if (i > 0) { // Do something } else // We know i is equal to 0 { // Do something }
An Example of an Internal Invariant (cont.)
Back SMYC Forward

One Approach:

if (i > 0) { // Do something } else { assert i == 0 : i; // Do something }

Another Approach:

assert i >= 0 : i; if (i > 0) { // Do something } else { // Do something }
A Concrete Example of an Internal Invariant
Back SMYC Forward

The Original Code Ignoring the Invariant:

if (delta > 0) total += delta;

Alternative Code Ignoring the Invariant:

total += Math.max(0, delta);

Taking Advantage of the Invariant Using an Assertion:

assert delta >= 0 : delta; total += delta;
An Example of a Control-Flow Invariant
Back SMYC Forward

This fragment assumes that there are only four suits.

switch(suit) { case Suit.CLUBS: // Do something break; case Suit.DIAMONDS: // Do something break; case Suit.HEARTS: // Do something break; case Suit.SPADES: // Do something break; default: // Shouldn't get here }
An Example of a Control-Flow Invariant (cont.)
Back SMYC Forward

Using an assertion

switch(suit) { case Suit.CLUBS: // Do something break; case Suit.DIAMONDS: // Do something break; case Suit.HEARTS: // Do something break; case Suit.SPADES: // Do something break; default: assert false : suit; }
The Other Uses Explained
Back SMYC Forward
  • Precondition:
    • Something that must be true when a method is invoked
  • Postcondition:
    • Something that must be true after a method completes successfully
  • Class Invariant:
    • Something that must be true about each instance of a class
There's Always More to Learn
Back -