Record Class ConstructVerdict

java.lang.Object
java.lang.Record
org.ek9lang.compiler.symbolic.ConstructVerdict
Record Components:
constructFqn - the fully qualified name of the analysed construct
verified - true when no counterexample was found within the bounded model
counterexamples - the undischarged obligations refuted by a concrete input
deadBranches - the branches proven unreachable for every input (discharged by contradiction)
provedSafe - the obligations the engine discharged — proved cannot fail (the green ✓ list: a literal divisor, a require/if guard, a constrained value that stays in window). As the addendum argues, the proved-safe list matters as much as the failures — it is what turns "no counterexample" into "positively verified here, and here's why" in the IDE Flow pane. Distinct from deadBranches (a whole branch is unreachable) and from the silently-skipped sites the engine cannot model either way.
unanalysableReason - why the engine could not analyse this construct at all, or null when it did. Non-null forces verified false — see notAnalysed(String, String).
public record ConstructVerdict(String constructFqn, boolean verified, List<ConstructVerdict.Counterexample> counterexamples, List<ConstructVerdict.DeadBranch> deadBranches, List<ConstructVerdict.ProvedSafe> provedSafe, String unanalysableReason) extends Record
The result of running the Symbolic/Contract engine (SymbolicEngine) over one construct (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3/§4.4/§6). It is the ∃-polarity payoff of the scanner: the M1 census (Layer 1) says how many obligations a construct carries and how many an existing analysis already discharges; this verdict says, for the undischarged ones, whether a concrete input refutes them and, if so, what that witnessing input is.

Two independent signals are folded together here — this is the tie of the two M3 engine cores:

  • Dead branches from the phase5.flow.SymbolicPathConditionWalker (slice A): a branch whose accumulated relational facts are unsatisfiable is unreachable for every input, so any obligation it guards is discharged by construction (Example 6: require lo <= hi then if lo > hi — the if body is dead).
  • Counterexamples from the WitnessEnumerator (slice B): an undischarged obligation driven through a type's representative value-classes, yielding the first input that violates it (Example 1: total / count — count=0).

A construct is verified() exactly when the engine analysed it and found no counterexample to any of its obligations within the bounded model. This is the value asserted by the @Verified directive; each ConstructVerdict.Counterexample.witness() is the value asserted by @Counterexample (§4.2).

"No counterexample" is not the same as "verified". When the engine cannot reach a construct's body at all it must say so, never fall through to a green light: an empty counterexample list would otherwise self-certify a body that was never read. notAnalysed(String, String) is that third outcome, and the compact constructor makes the bad state unrepresentable — a verdict carrying an unanalysableReason() can never also be verified. This is the eliminate, don't mitigate rule applied to the verdict itself.

  • Constructor Details

  • Method Details

    • notAnalysed

      public static ConstructVerdict notAnalysed(String constructFqn, String reason)
      The verdict for a construct whose body the bounded model could not reach — not a pass. Carries no counterexamples because none were looked for, which is precisely why it must not be reported as verified.
      Parameters:
      constructFqn - the fully qualified name of the construct that could not be analysed
      reason - why it could not be analysed, in terms a developer can act on
      Returns:
      a verdict that is neither verified nor refuted

    • analysed

      public boolean analysed()
      Whether the engine actually read this construct's body (false = no claim either way).

    • hasCounterexample

      public boolean hasCounterexample()
      Whether the engine refuted at least one obligation with a concrete counterexample.

    • toString

      public final String toString()
      Returns a string representation of this record class. The representation contains the name of the class, followed by the name and value of each of the record components.
      Specified by:
      toString in class Record
      Returns:
      a string representation of this object

    • hashCode

      public final int hashCode()
      Returns a hash code value for this object. The value is derived from the hash code of each of the record components.
      Specified by:
      hashCode in class Record
      Returns:
      a hash code value for this object

    • equals

      public final boolean equals(Object o)
      Indicates whether some other object is "equal to" this one. The objects are equal if the other object is of the same class and if all the record components are equal. Reference components are compared with Objects::equals(Object,Object); primitive components are compared with the compare method from their corresponding wrapper classes.
      Specified by:
      equals in class Record
      Parameters:
      o - the object with which to compare
      Returns:
      true if this object is the same as the o argument; false otherwise.

    • constructFqn

      public String constructFqn()
      Returns the value of the constructFqn record component.
      Returns:
      the value of the constructFqn record component

    • verified

      public boolean verified()
      Returns the value of the verified record component.
      Returns:
      the value of the verified record component

    • counterexamples

      public List<ConstructVerdict.Counterexample> counterexamples()
      Returns the value of the counterexamples record component.
      Returns:
      the value of the counterexamples record component

    • deadBranches

      public List<ConstructVerdict.DeadBranch> deadBranches()
      Returns the value of the deadBranches record component.
      Returns:
      the value of the deadBranches record component

    • provedSafe

      public List<ConstructVerdict.ProvedSafe> provedSafe()
      Returns the value of the provedSafe record component.
      Returns:
      the value of the provedSafe record component

    • unanalysableReason

      public String unanalysableReason()
      Returns the value of the unanalysableReason record component.
      Returns:
      the value of the unanalysableReason record component