Class CriticalValues

java.lang.Object
org.ek9lang.compiler.symbolic.CriticalValues
public final class CriticalValues extends Object
THE registry of "dangerous values" per obligation kind for the Symbolic/Contract engine — the single place that answers which concrete base-domain values would violate this obligation. Call this; do not re-derive a value != 0 test inline.

It is the pivot of the type-domain discharge principle: a constrained type is an admissible value-set; each obligation is a dangerous value-set; if they are disjoint the obligation is discharged for every value of that type — by construction, everywhere, proven once off the type (no caller analysis; see SymbolicEngine.classifyDivision(EK9Parser.ExpressionContext, Set, FunctionSummary)). This class defines the dangerous set ONCE and derives from it both directions the engine needs:

  • safe(String) — the safety predicate the WitnessEnumerator drives to find a refuting witness (the first value that IS dangerous), and
  • windowExcludesAll(long[], String) — the disjointness test proving a constrained type's inclusive [lo,hi] window contains none of the dangerous values (→ proved-safe).

Extend by adding a row: an obligation kind maps to its critical values in the shared numeric (Integer/Float) domain. DIV_BY_ZERO -> {0} is the seed; sqrt/log domain, index lower-bound, overflow near the extremes, … are the same shape (a dangerous set), each one row here — the engine's discharge/refute logic then applies unchanged.

  • Method Details

    • dangerousValues

      public static long[] dangerousValues(String obligation)
      The base-domain values that would violate obligation, or empty when none are modelled.

    • safe

      public static LongPredicate safe(String obligation)
      The safety predicate for obligation: true for a value that does NOT violate it. The WitnessEnumerator returns the first pool/window value for which this is false — the refuting witness (e.g. 0 for a division).

    • windowExcludesAll

      public static boolean windowExcludesAll(long[] window, String obligation)
      Whether the inclusive window [lo,hi] a constrained type narrows to contains NONE of obligation's dangerous values — i.e. the type forbids every value that would break it, so the obligation is discharged for every value of the type. An obligation with no modelled dangerous values is vacuously excluded (returns true), so callers should gate on a decidable window first.