| Class | Description |
|---|---|
| MethodVariantSupport | Runtime support for a method-level Decreases recursion termination measure. |
| 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). |