BDD as Specification: A Case Study in Deriving Code from Scenarios

A companion to TDD & BDD, which covers the Given/When/Then cycle and its tooling ecosystem in general. This page goes one layer deeper on a single claim that page only asserts: that a well-written BDD scenario isn't just a test, it's a specification precise enough to derive an implementation from — and grounds that claim in a real, working system rather than a hypothetical. Two real case studies ground it: PatLang's inductive synthesis engine (full technical writeup here), which derives a rule symbolically from scenarios with no LLM involved, and a genuinely different mechanism, an LLM-driven self-healing code synthesizer, which uses BDD scenarios as the actual pass/fail oracle for code it writes. Both are paired, separately, with the language's design-by-contract mechanism — three genuinely distinct pieces used together, not one fused pipeline, and this page is careful to keep that distinction honest throughout.

A Given/When/Then scenario is already labelled training data

Most treatments of BDD stop at "scenarios are executable documentation." That's true, but understates what a well-formed scenario actually contains. Given is background knowledge — the world-state a hypothesis has to be consistent with. When is the input being classified or acted on. Then is the expected output — exactly the ground-truth label a learning system needs. That's precisely the (background facts, positive/negative examples) → rule shape every inductive logic programming system takes as input. A product owner writing scenarios in plain English is, without necessarily meaning to, authoring a labelled dataset. Nobody has to hand-translate "the system should do X when Y" into that shape — a properly written scenario already is that shape.

Case study: deriving a rule from scenarios, and diagnosing a gap in them

The classic inductive-logic-programming benchmark is "grandparent," derived here from nothing but background facts and Given/Then examples, using PatLang's real self_hosting/lib/synthesis_lgg.patlang module:

# Given (background facts)
parent(alice, bob).    parent(bob, carol).
parent(dave, erin).    parent(erin, frank).

# Then (labelled examples)
grandparent(alice) should hold.
grandparent(dave) should hold.

The engine doesn't guess a template and test it blindly — it walks the background-fact graph outward from each positive example to find a real, witnessed chain of relations connecting it to something, then generalizes across examples by taking the longest common prefix of their chains. That prefix-taking is genuine anti-unification: the terms being generalized are relation sequences, and the point where two examples' evidence diverges is exactly where generalization has to stop. From the two examples above, it derives:

rule grandparent(X) :- parent(X, Y), parent(Y, Z).

That's the interesting case. The genuinely useful case is what happens when a scenario can't be satisfied. Add a third example the background facts don't support:

grandparent(isaac) should hold.
# ...but no "parent" fact anywhere mentions isaac.

A test framework would report this as a failure. This engine returns a tagged diagnosis, and turns that diagnosis into an actual question addressed to whoever wrote the scenario:

> diagnosis
["no_witness", ["isaac"]]

> question
"The scenarios say grandparent(\"isaac\") should hold, but no background fact
 connects \"isaac\" to anything at all. Is a fact about \"isaac\" missing from
 the background knowledge, or should this scenario be removed?"

The opposite mistake gets an equally specific question. A negative example sharing the identical witnessed chain as the positives (a real-world distinction the given facts simply don't capture) comes back as:

> diagnosis
["conflict", [["grandparent", "eve", false,
  "negative example wrongly covered by the induced rule -- background facts
   don't yet distinguish it from the positives"]]]

> question
"The induced rule also matches \"eve\", but the scenarios say
 grandparent(\"eve\") should NOT hold. Is there a background fact that
 distinguishes \"eve\" from the positive examples that's missing, or is an
 additional condition needed?"

Both questions name the exact example at fault and the exact kind of gap (missing evidence vs. missing distinction) — the difference between a test suite that reports "3 failed" and one that tells a reader what to go check first. This is what "BDD scenarios are precise enough to derive an implementation from" looks like when taken all the way: not just generating code from a spec, but generating a specific, answerable question when the spec itself is the thing that's incomplete.

A second case study: BDD as the verification oracle for LLM-synthesized code

The grandparent example derives a rule symbolically, with no LLM involved at all. A genuinely different mechanism, PatLang's friendly_cli/lib/self_healing_engine.patlang, uses BDD scenarios in a different but equally load-bearing role: as the actual pass/fail oracle for code that fills a gap the system can't otherwise plan its way around. When a needed host function is missing, the engine runs RED → PLAN → GREEN. RED writes the BDD spec first and confirms the implementation doesn't exist yet:

Feature: Synthesized Function Verification
Scenario: Validate synthesized tool
  Given a target test file on disk
  When the synthesized function is executed
  Then the contract and output are verified

PLAN is deliberately the step before ever asking an LLM anything: the design intent is to first search for an existing GOAP action (see the goal-oriented planning demo) that already satisfies the BDD spec, so a gap the system can already plan its way around never needs an LLM call at all — an LLM is meant to be the fallback for what genuinely can't be composed from what already exists, not the default path. Worth being honest about the current state, not the aspiration: that GOAP-planning step is still a stub in the code today (marked with its own TODO), so every call currently falls straight through to the LLM. The RED/GREEN verification discipline described below applies regardless of which path eventually supplies the implementation, but the "ask an LLM only as a last resort" framing is the intended design, not yet the enforced behaviour.

Whichever path supplies it, an implementation is compiled together with the SAME spec written during RED, run for real, and the compiled program's own reported result is the verdict — not "the output looked plausible," an actual executed BDD run deciding pass or fail.

Two real bugs found while building this are worth naming, because both are exactly the shape of mistake this page is otherwise warning against — a spec that looks like it verifies something but doesn't. First, the GREEN phase originally checked for the substring "CONTRACT PASS" in the compiled program's output — but that string was printed unconditionally by the synthesized function's own generated code, before the actual postcondition check even ran, so it was present whether or not the synthesized function was correct. A direct repro (deliberately supplying a wrong expected result) still reported success. The fix checks for the BDD framework's own t_report() summary line ("ALL TESTS PASSED", and explicitly the absence of "TESTS FAILED") — the one signal that's actually tied to every check() in the inner run, including the postcondition. Second, the postcondition itself silently could never pass for either existing scenario: the synthesized value was a number, the expected result was embedded as a string literal, and this language has no implicit numeric-to-string coercion, so the comparison was always false regardless of correctness — invisible until the first bug was fixed and a previously "passing" scenario suddenly, correctly, started failing. The lesson generalizes past this one engine: a BDD scenario is only as trustworthy as the thing that actually decides pass/fail inside it — "the compiled program produced output" and "the compiled program's own tests genuinely passed" are different claims, and it's worth checking which one your tooling is actually verifying.

Contracts specify the boundary; scenarios specify the behaviour — two mechanisms, used together

It would be neat if the story ended with "and then contracts feed straight into the induction engine" — but that's not how the actual system works, and this page would rather be honestly incomplete than imply a pipeline that doesn't exist. PatLang has a real design-by-contract mechanism, require/ensure/assert, all lowering to one contract_check host call, enforced identically whether interpreted, compiled, or run in WebAssembly:

make a function called safe_divide takes a, b returns r
  require b != 0
  let r = a / b
  ensure (r * b) == a
  return r
end

This is a genuinely separate mechanism from the induction engine above, and the two are used together rather than fused: a BDD scenario plus induction derives what the rule's logic should be (the grandparent example above); a contract on the function that uses that rule specifies what must hold at its boundary regardless of how the body is implemented — a precondition the caller must satisfy, a postcondition the body must guarantee, checked identically whether that body was hand-written or induced. Treat them as two different questions a specification answers: "what should this compute, given these examples" (BDD + induction) and "what must always be true going in and coming out, no matter how it's computed" (contracts). A rule induced from scenarios that violates a contract is a genuine, catchable bug — the contract doesn't care where the rule came from.

What actually has to be true for this to work

None of this is free, and overselling it would undercut the honest framing this page is trying to keep. It requires: background facts and scenarios that are actually consistent (the engine can tell you when they're not, but it can't fix contradictory requirements for you); a domain where the target relationship really does have witnessed structure in the background facts (a rule with no connection to anything the facts describe can't be discovered, only guessed); and — a real, still-open limitation, not glossed over — a search space that stays tractable, since the clustering step behind disjunctive rules (two unrelated reasons the same predicate should hold) is a heuristic, not a guaranteed-optimal solver, and an adversarial domain could still beat it. See the full writeup's honest limits section for the complete, current list.

A short checklist

Does your Given/When/Then scenario actually separate background knowledge (Given) from the specific input (When) from the expected label (Then) — or has some of the "given" quietly leaked into the "when," making the scenario harder to generalize from than it looks?
If a scenario can't be satisfied by your current understanding of the system, does your tooling tell you which example is the problem and what kind of gap it represents — or just that something failed?
Are you treating "what should this compute" and "what must always hold regardless of implementation" as the same question? They're not — a contract on a function's boundary is worth having even when (especially when) you're not sure the body's logic is complete yet.
Before claiming a specification technique lets you "derive the code," have you actually run it against a case where the specification is incomplete or contradictory, and confirmed it fails informatively rather than silently?