Package org.ek9lang.compiler.symbolic

package org.ek9lang.compiler.symbolic
  • Class
    Description
    ConstructVerdict
    The result of running the Symbolic/Contract engine (SymbolicEngine) over one construct (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3/§4.4/§6).
    ConstructVerdict.Counterexample
    A concrete input that violates an obligation — the witness a developer can paste into a test.
    ConstructVerdict.DeadBranch
    A branch proven dead (unreachable for every input) by a contradiction in its path condition.
    FunctionSummary
    The inter-procedural summary of a callable (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3.4) — the facts about it a caller needs to reason across the call boundary without re-analysing its whole body.
    FunctionSummary.RequirePredicate
    A single require precondition: param OP literal, keyed to the parameter's position so a call site can map it onto the matching argument.
    SymbolicAnalysis
    SINGLE THREADED The Layer-2 symbolic/contract verification pass (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §4.4).
    SymbolicEngine
    The Layer-2 symbolic engine of the Symbolic/Contract Scanner (M3/M4) — it turns "this construct carries undischarged obligations" (the M1 census verdict) into "here is the exact input that panics", or proves no such input exists within the bounded model (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3/§11.2/§12).
    WitnessEnumerator
    The bounded-model witness materialiser for the Symbolic/Contract scanner (M3): given an obligation expressed as a predicate over a candidate input, enumerate the representative value-classes of a type and return the first input that violates it — a concrete counterexample.
    WitnessEnumerator.Witness
    A concrete counterexample: which value-class it came from, its EK9-source literal, and its value.