| Class | Description |
|---|---|
| MethodVariantSupport | Runtime support for a method-level Decreases recursion termination measure. |
| ThrowsIfSupport | Runtime support for checked @ThrowsIf arm-sets (invoked from
generated code; not intended to be called by user code). |
| VariantSupport | Shared runtime support for Decreases termination
measures, used by both the loop variant (@Decreases on a loop) and the
recursion variant (@Decreases on a method, via MethodVariantSupport). |
| ViolationTracker |
| Exception | Description |
|---|---|
| CircularAssertionCallException |
| Error | Description |
|---|---|
| AssertionViolation | |
| ClassInvariantViolation | |
| LoopInvariantViolation | |
| LoopVariantViolation | Thrown whenever a loop variant (decreases/increases) violation occurs. |
| PostconditionViolation | |
| PreconditionViolation | |
| RecursionVariantViolation | Thrown when a method-level Decreases recursion termination measure fails — either a recursive re-entry did not strictly decrease the measure, or the measure became negative (not well-founded). |
| ThrowsIfViolation | Thrown whenever a @ThrowsIf exceptional-contract violation is detected
by a checked arm-set: the method returned normally although a
must-throw condition held, or threw a matching exception although no arm's
condition held (the latter checked only for exhaustive arm-sets). |