Features

• Class invariants.
• Pre conditions.
• Post conditions, with access to return- and pre- values.
• Access to private members of the tested class from the contract implementation.
• Automatic detection of simple getters (i.e. "pure" methods, that don't change state), where no class invariant verifications are necessary.
• It is possible to explicit mark methods as "pure" (even methods defined in interfaces).
• Inheritance of contracts, i.e. extending classes inherit the parent's contracts, also overridden methods.
• Contract refinement, i.e. extending classes may define their own contracts in which case they are merged according to DBC theory.
• Contracts for interfaces, i.e. define a contract for an Interface and all implementing classes (and their sub classes) will verify the contract.
• Combinations of "interface contracts" and "class contracts", works like contract refinement.
• Logging of contract verifications, it is possible to register loggers that are notified when contracts are verified, e.g. to support statistics gathering.
• Possibility to debug contracts in your favorite IDE.