A unique exception should be thrown when an invariant is violated

[tdegueul]

In @Contracted, invariants and pre/postconditions checks are currently mixed. Thus, a violated invariant will result in either a PreConditionViolationException or PostConditionViolationException, depending on whether the violation occurs when calling or exiting a given method.

@Contracted should check invariants separately and throw an appropriate InvariantViolationException.