What is EK9's Symbolic (Contract) analysis and how do I read the Flow pane's Symbolic mode?

  COUNTEREXAMPLE (must-fix): a witnessing input that panics or is silently unset. Example: 'total / quantity' is refuted by quantity=0.
  PROVED-SAFE (green): the obligation is discharged - it cannot fail. A division is proved-safe when the divisor is a non-zero literal, is dominated by a 'require x <> 0' (or an enclosing 'if x <> 0' guard), or has a constrained TYPE whose window excludes 0 (e.g. 'Quantity as Integer constrain as > 0').

  DIV_BY_ZERO             - a division/mod/rem by a value that can be zero.
  CALLEE_REQUIRE          - a call whose argument breaks the callee's 'require' precondition.
  CONSTRAINED_CONSTRUCTION- a constrained-type construction whose value can leave the type's window.

  IDE Flow Analysis pane -> tick 'Symbolic analysis' (default off). You get a summary strip (N must-fix, N advisory, N proved-safe), a Contract-findings list with the witness and a paste-ready @Test, and a detail drawer. Each obligation line also gets an 'S' badge in the editor gutter (hover it for the verdict) - scoped to the function you are analysing.
  '+ Add as @Test' generates a verify-directed @Test that pins the boundary (same engine as ek9_generate_edge_case_tests).
  AI / CLI: the ek9_verify_method tool returns the verdict for a function.
  Build: 'ek9 -Xverify' runs the SYMBOLIC_ANALYSIS phase, checks any @Verified / @Counterexample directives, and colours the Contract roundel in the -t6 quality report.

  1. Guard it with a precondition: add 'require quantity <> 0'. IMPORTANT - a return's inline initialiser runs BEFORE any require, so to guard the computation declare the return uninitialised ('rtn as Integer?') and assign it AFTER the require (see safeUnitPrice below). Guard first, compute second.
  2. Lift the value to a constrained type ('Quantity as Integer constrain as > 0'). The invariant then lives on the TYPE: you cannot construct a Quantity of 0, so every function taking a Quantity is safe by construction and no require is needed. The scanner reads the constraint window off the type and proves the division safe.

defines module qa.dataflowsafety.symbolicanalysis

  defines function

    //COUNTEREXAMPLE quantity=0: dividing by a free parameter is a silent unset - the Symbolic engine
    //finds the witnessing input and offers a directed @Test in the Flow pane.
    unitPrice()
      ->
        total as Integer
        quantity as Integer
      <- rtn as Integer: total / quantity

    //PROVED-SAFE: the require dominates the division. The return is declared uninitialised ('as Integer?')
    //and assigned AFTER the require, so the guard runs before the computation (guard first, compute second).
    safeUnitPrice()
      ->
        total as Integer
        quantity as Integer
      <- rtn as Integer?
      require quantity <> 0
      rtn: total / quantity