ek9_verify_method

Answers first: status, name, verified, then counterexampleCount, counterexamples[] {obligation, witness, suggestedTest, suggestedFix}, provedSafe, deadBranches and nextStep.

Category: Enquiry · Compare: Design-by-contract / bounded-model verifier (Dafny, Frama-C, CBMC)

When to use it

'Can any input break this function's contract - a panic or an unset result' is one call with symbol:'name' - no file needed; the breaking input is returned.

When not to use it

internal control flow or complexity of a body, not contract safety (use ek9_query_flow)
materialising a returned counterexample as an actual failing test (use ek9_generate_edge_case_tests)
discharging a returned counterexample by inserting the suggested require (use ek9_apply_symbolic_fix)
the every-build census rollup across the whole workspace (use ek9_run_tests with generateReport:true - the quality report's Contract roundel)

Details

Runs the SymbolicEngine on demand against the already-resolved program (after PRE_IR_CHECKS — no -Xverify flag, no IR), resolving the ENCLOSING FUNCTION from the anchor; a type/record/bare-expression target returns status:'not-found' (re-anchor on the function) and a dynamic function returns status:'not-applicable' (no verification claim either way - its captures are constructor-injected fields, not free inputs). verified means verified TO A BOUND (finite value-class enumeration + affine boundaries from requires) — advisory, never fails a build. counterexamples[] carry {obligation, witness as name=value, line}, enriched with suggestedTest, suggestedFix (the discharging require — its presence gates ek9_apply_symbolic_fix) and alreadyTested/testProgram when an existing @Test already pins that boundary; obligation kinds today are DIV_BY_ZERO (silently-unset result), CALLEE_REQUIRE (a callee's require violated across a call) and CONSTRAINED_CONSTRUCTION (constructed value can leave the constrained type's window); provedSafe[] lists obligations proven unbreakable and deadBranches[] {reason} branches unreachable for every input.

Arguments

Argument	Type	What it is
`file`	string	The EK9 source file - OPTIONAL when symbol is a construct name; required to anchor on a member or a use site.
`line`	integer	1-based line inside the function's body or on its declaration - OMIT it and pass symbol:'name' to let the tool find the line (a model counting lines miscounts).
`symbol`	string	A construct NAME alone ('Shape', 'sample.deps.core::Validator') - no file needed, the tool finds it workspace-wide; or, with file (+ line), the identifier you mean there.

Recorded calls

Real calls, recorded against small projects and checked on every build - a changed answer fails it.

Verify dynamic not analysable

Request

{
  "file" : "Dynamic.ek9",
  "line" : 12
}

Response

{
  "declaredAt" : {
    "file" : "Dynamic.ek9",
    "line" : 11
  },
  "fullyQualifiedName" : "com.example.dynamic::fn",
  "meta" : {
    "serverMs" : "<timing>"
  },
  "name" : "fn",
  "note" : "a dynamic function has no named declaration to analyse, and its captured variables are constructor-injected fields rather than free inputs — the bounded model does not cover it",
  "status" : "not-applicable",
  "summary" : "Not analysable — no verification claim is made either way: a dynamic function has no named declaration to analyse, and its captured variables are constructor-injected fields rather than free inputs — the bounded model does not cover it.",
  "verified" : false
}

Verify shape

Request

{
  "file" : "Maths.ek9",
  "line" : 5
}

Response

{
  "counterexampleCount" : 1,
  "counterexamples" : [ {
    "line" : 9,
    "obligation" : "DIV_BY_ZERO",
    "suggestedFix" : {
      "kind" : "GUARD",
      "label" : "Add require count <> 0 (callers passing 0 will now Panic)",
      "obligation" : "DIV_BY_ZERO",
      "require" : "require count <> 0"
    },
    "suggestedTest" : "@Test\nSafeAverageUnsetWhenCount0()\n  result <- safeAverage(1, 0)\n  assert not result?",
    "witness" : "count=0"
  } ],
  "deadBranches" : [ ],
  "declaredAt" : {
    "file" : "Maths.ek9",
    "line" : 5
  },
  "fullyQualifiedName" : "com.example.verify::safeAverage",
  "meta" : {
    "serverMs" : "<timing>"
  },
  "name" : "safeAverage",
...

Cut short here: 6 more lines. The whole recorded call.