Class CounterexampleDirective

java.lang.Object

org.ek9lang.compiler.directives.ResolutionDirective

org.ek9lang.compiler.directives.CounterexampleDirective

All Implemented Interfaces:

Directive

public class CounterexampleDirective
extends ResolutionDirective

Compiler self-verification directive (NOT an end-user feature) asserting that the Layer-2 symbolic engine found a specific witnessing input for a construct (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §4). Lives only in the compiler's own .ek9 test fixtures, exactly like @Obligations, to pin the counterexample search. Checked at the SYMBOLIC_ANALYSIS phase, which only runs under -Xverify.

The asserted value is the quoted witness as name=value; the check passes when it is one of the construct's squirrelled counterexamples:

 @Counterexample: SYMBOLIC_ANALYSIS: FUNCTION: "com.acme::safeAverage": "count=0" 

Constructor Summary

Constructors

Constructor	Description
CounterexampleDirective(DirectiveSpec spec)	The Directive to test a squirrelled symbolic counterexample witness in EK9 instrumented code.

Method Summary

Modifier and Type	Method	Description
DirectiveType	type()	What s the type of the directive.

Methods inherited from class ResolutionDirective

getAdditionalName, getAppliesToLineNumber, getDirectiveToken, getSymbolCategory, getSymbolName, getSymbolSearch, isForPhase, isForVariable, toString

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Details

CounterexampleDirective

public CounterexampleDirective(DirectiveSpec spec)

The Directive to test a squirrelled symbolic counterexample witness in EK9 instrumented code.

Method Details

type

public DirectiveType type()

Description copied from interface: Directive

What s the type of the directive.