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)

public record ConstructVerdict(String constructFqn, boolean verified, List<ConstructVerdict.Counterexample> counterexamples, List<ConstructVerdict.DeadBranch> deadBranches)
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 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).

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final record	ConstructVerdict.Counterexample	A concrete input that violates an obligation — the witness a developer can paste into a test.
static final record	ConstructVerdict.DeadBranch	A branch proven dead (unreachable for every input) by a contradiction in its path condition.

Constructor Summary

Constructors

Constructor	Description
ConstructVerdict(String constructFqn, boolean verified, List<ConstructVerdict.Counterexample> counterexamples, List<ConstructVerdict.DeadBranch> deadBranches)	Creates an instance of a ConstructVerdict record class.

Method Summary

Modifier and Type	Method	Description
String	constructFqn()	Returns the value of the constructFqn record component.
List<ConstructVerdict.Counterexample>	counterexamples()	Returns the value of the counterexamples record component.
List<ConstructVerdict.DeadBranch>	deadBranches()	Returns the value of the deadBranches record component.
final boolean	equals(Object o)	Indicates whether some other object is "equal to" this one.
boolean	hasCounterexample()	Whether the engine refuted at least one obligation with a concrete counterexample.
final int	hashCode()	Returns a hash code value for this object.
final String	toString()	Returns a string representation of this record class.
boolean	verified()	Returns the value of the verified record component.

Methods inherited from class Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Details

ConstructVerdict

public ConstructVerdict(String constructFqn,
 boolean verified,
 List<ConstructVerdict.Counterexample> counterexamples,
 List<ConstructVerdict.DeadBranch> deadBranches)

Creates an instance of a ConstructVerdict record class.

Parameters:

constructFqn - the value for the constructFqn record component

verified - the value for the verified record component

counterexamples - the value for the counterexamples record component

deadBranches - the value for the deadBranches record component

Method Details

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