Download

A version of jaxen with added invariant checkers can be downloaded here.

Requirements

To run the instrumented version of jaxen, you need the following software on your system:
  • A Java 1.6 Runtime Environment
  • Tthe ant build tool

Contents

The archive contains the follwing files:
  • An ant build file to execute test
  • The files CHECKED-invariantCheckers.ser and field_visibility.ser are needed by the invariant checker framework
  • The jar/ directory contains all jars that are needed to execute jaxen with the added invariant checkers.
  • The doc/ directory contains this documentation
  • The src/ directory contains an unmodified distribution of jaxen 1.1.1
  • The xml/ directory contains files that are needed to execute the JUnit Tests

Run

Run Tests

The normal test suite of Jaxen can be run with the test ant task.
ant test
The test suite should not violate any invariant, since the dynamic invariants where learned from this test suite. The output should indicate that all tests pass:
Buildfile: build.xml

test:
[junit] Running org.jaxen.test.JaxenTestSuite
[junit] Tests run: 680, Failures: 0, Errors: 0, Time elapsed: 5.636 sec

BUILD SUCCESSFUL
Total time: 6 seconds

Violate Invariants

An additional test that is designed to violate invariants can be run with the testInvariantViolations ant task.
ant testInvariantViolations
This should produce an output like this:
testInvariantViolations:
[junit] Running org.jaxen.test.InvariantViolationTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 0.807 sec
[junit] 0 INFO [run - de.unisb.cs.st.javalanche.invariants.runtime.InvariantObserver$1] - Ids of violated invariants: [3658, 101, 16590, 3620, 3651, 94, 3879, 6697, 134]
[junit] 3 INFO [run - de.unisb.cs.st.javalanche.invariants.runtime.InvariantObserver$1] - Total invariant violations: 9
[junit] 3 INFO [run - de.unisb.cs.st.javalanche.invariants.runtime.InvariantObserver$1] - Different invariants violated: 9
With the ant task testInvariantViolationsVerboseSummary a more verbose summary is printed.