public final class VariantSupport
extends Object 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).
It is the single source of truth for what "strictly decreases and stays
well-founded" means — a scalar Comparable (with a non-negative floor for
Numbers) or a List compared lexicographically — and for whether
the check runs at all under the -ea/-da configuration.
The comparison itself is violation-agnostic (describeFailure returns a
description rather than throwing) so each caller can raise the appropriate
violation type.
| Type Params | Return Type | Name and description |
|---|---|---|
|
public static void |
checkLoopVariant(Object prev, Object curr, String className)Loop-variant entry point invoked from generated loop-body code: if enabled, verify curr strictly decreased from prev and stayed
well-founded, throwing LoopVariantViolation otherwise. |
|
public static String |
describeFailure(Object prev, Object curr)Describe how curr fails to be a valid strict, well-founded decrease
from prev, or null if it is valid. |
|
public static boolean |
enabled(String className)Whether termination-measure checks are enabled for className under the
current -ea/-da configuration (a null class name uses
the global default). |
Loop-variant entry point invoked from generated loop-body code: if enabled,
verify curr strictly decreased from prev and stayed
well-founded, throwing LoopVariantViolation otherwise.
prev - the variant before the iterationcurr - the variant after the iterationclassName - the enclosing class name (for -ea/-da gating) Describe how curr fails to be a valid strict, well-founded decrease
from prev, or null if it is valid. List measures are
compared lexicographically.
prev - the measure beforecurr - the measure afternull if the decrease is valid Whether termination-measure checks are enabled for className under the
current -ea/-da configuration (a null class name uses
the global default). Mirrors how @Requires/@Ensures gate.
className - the enclosing class name, or null for the global defaulttrue if the check should run