- Allows a developer to define class invariants (@Invar), method
preconditions (@Pre), and method postconditions (@Post).
- Conditions are defined as java boolean statements.
- Class inheritance and interface implementation is supported for the
entire inheritance tree.
- Precondition contravariance and postcondition covariance is handled.
- Contract conditions are defined as single statements or an array of
statements so the developer doesn't have to "&&" multiple contract conditions
together into a single statement. This also facilitates messages explicitly
identifying which contract conditional is violated at runtime.
- Uses $pre, $return, $for, and $implies keywords to simplify conract definition.
- $pre([type of value to capture], [value to capture or expression]) - used in a @Post condition to capture a value at the beginning of a method call for use in a comparison at the end of the method call
- $return - used in a @Post condition to capture the return value of the method
- $for([Java 5 for loop control statement]) [boolean conditional] - used to check a condition within a for loop, generally used for array or collection value conditions
- [if condition is true] $implies [other condition must be true] - used to simplify contract statements
- Allows package and class level filtering when generating instrumented code.
- Generates formatted readable java code.
- Compatable with the JDK 1.5 Annotation Processing Tool (apt.exe)
- Includes easy to use command line tool.