Last updated: 2026-09-26

U
Undergraduate level

Schemas and Scenarios: A Working Z/BDD Hybrid

Formal Methods covers a Z schema: a universally-quantified invariant, checkable independently of any one concrete case. BDD as Specification covers the opposite kind of claim: a Given/When/Then scenario is one concrete, witnessed example, useful precisely because it’s concrete, not despite it. This page connects them for real: a Z-style schema states a general invariant, and a set of Gherkin-style scenarios serve as its concrete witnesses, checked against each other rather than written and trusted independently. Every mechanism described below is built, tested, and runnable — the live examples further down run in this page, not on a build machine somewhere else. The libraries themselves are in the project’s GitHub repository, named zs_*.patlang.

Prior Art

This isn’t unclaimed territory. Bowen Liu’s research at the University of Waikato converts BDD-style behavioural specifications into first-order-logic predicates and checks them for consistency against formal models1. The follow-on PhD, supervised by Judy Bowen, Jessica Turner, and Steve Reeves, does this against Z specifications and applies it to the T34 syringe driver, a safety-critical medical device2. That thesis experiments with refinement of the Z specification and leaves it as open future work2.

Liu’s process is manual and works across two documents. An analyst extracts the essential facts from a feature’s scenarios, finds the matching statements in the Z specification, writes the Given and When conditions as first-order predicates, and states each as a temporal-logic assertion: in every state, if the predicates do not all hold, the operation is not enabled. The ProB model checker tests the assertion over the Z model and returns a counter-example when it fails2. The thesis states that the process finds inconsistencies between the two specifications and does not guarantee the correctness of the system2.

The idea of checking a Gherkin specification against a Z-style specification is Liu’s. Treating the scenarios as concrete witnesses of a schema, with a tagged diagnosis for each way a witness can fail, is our own formulation, and its mechanism is different. A schema here is executable PatLang held in the same source as its scenarios. One run checks each scenario’s before and after states against the invariant, the operation’s precondition, and its postcondition, and reports which of those four checks failed. Liu’s predicates come from the Given and When clauses, and the thesis excludes negative scenarios2, so postconditions and rejection scenarios sit outside that process. Running a synthesized function or a planner’s output against a schema has no counterpart in the thesis either.

A third piece of work sits between the other two. Lili Shao’s dissertation, also from Waikato and also supervised by Judy Bowen — who shared a copy of it directly — converts a real Z specification into Gherkin and then into Playwright scripts using an LLM at each step, run against a real deployed web system4. It is not yet listed in the university’s research repository. Where Liu formalises the Gherkin and checks it against Z with ProB, Shao trusts the LLM’s translation once it parses and reads plausibly, verifying it by a Gherkin-syntax check plus manually counting how much of the Z specification’s scenarios and assertions the generated code covers. Nothing checks that the generated Gherkin means what the Z specification says. Her second experiment names the same problem as this page’s live examples: neither Z nor Gherkin can predict the name of a real page element, so the generated Playwright tests failed entirely until the selectors were fixed by hand. She calls this the mapping problem and leaves a declarative mapping language between abstract concepts and concrete implementation elements as future work. Her own tests do something none of the mechanisms on this page do: they run against a deployed system and catch defects a static check cannot. Ours checks whether a scenario is true of the schema; hers checks whether the generated code executes.

The four live examples near the top of this page check the states their scenarios supply. A second layer, described under From Examples to Every Reachable State, declares a schema as text and checks it against every state it can reach, reproduces the check from Liu’s thesis on the thesis’s own vending machine, and runs live in the panel further down. Three differences remain in Liu’s favour:

  • Liu’s process is written against Z. The declared schemas use an ASCII notation with sets, maps, and quantifiers, and have no schema calculus and no unbounded types.
  • Liu’s analyst finds the statements in the Z specification that match each phrase in a scenario. Here the analyst writes that correspondence down as fact and goal lines, and the check runs from there.
  • Exploration covers the states reachable from one initial state through finite input domains that the schema declares, and it needs each operation’s ensure clauses to define its after-state. ProB works over the Z model itself.

Two Kinds of Claim, Briefly FoundationalKnowledge that endures for decades — core principles

A Z schema states what must hold for every input satisfying its precondition — a BorrowBook schema states that any title already in books and not already in borrowedBy leads to a specific update, for every such title and member, not just one. A BDD scenario states one specific, concrete case; BDD as Specification is explicit that this is deliberate — a scenario is training data and a pass/fail oracle precisely because it’s concrete. Neither substitutes for the other. That’s exactly why keeping them consistent with each other is worth doing rather than assuming it happens for free.

Design notes on two choices behind this mechanism — why a schema’s clauses are ordinary compiled functions rather than inline text, and a checklist of what each stage needed — are on a separate page.

Try It Yourself: The Mechanism, Live

The four examples below run entirely in this page — the same self-hosted PatLang compiler and interpreter compiled to WebAssembly that powers every other live demo on this site, with the new pset/pmap/schema_bdd libraries inlined directly into the source (there’s no real filesystem in the browser sandbox, so include isn’t available here — everything the example needs is in the one block of text below). The last two examples carry more with them than the first two: the planner example needs plan_with_state, and the inductive-synthesis example includes the lexer, parser and lowerer as well, because the induction engine compiles each candidate rule into a small test script and runs it. Pick an example from the dropdown, edit it if you like, and press Run.

(not run yet)

The Negative Case: Catching a Scenario Before It Runs Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

Run the first example (one operation, one violation) and look at its second scenario: Given already states that “Dune” is borrowed by S. Okonkwo, then When has A. Diallo try to borrow it too. Checked against BorrowBook’s schema rather than run against any implementation, this fails before any code executes at all — its own Given already violates the operation’s precondition. That’s the mechanism’s whole point: schema_check returns a tagged diagnosis, ["precondition_violated", [op, state_before, inputs]], and schema_format_diagnosis turns it into a real, specific question rather than a bare pass/fail — mirroring the same tagged-diagnosis-plus-question pattern BDD as Specification’s induction engine already uses for a scenario a rule can’t satisfy:

> schema_check("LibraryLoans", "BorrowBook")
["precondition_violated", ["BorrowBook", [...], ["Dune", "A. Diallo"]]]

> schema_format_diagnosis("LibraryLoans", "BorrowBook", diagnosis)
["Scenario claims BorrowBook can run from this Given, but BorrowBook's own
 precondition returned false for these inputs. Is the Given wrong, or is
 BorrowBook's precondition too strict -- or is this scenario meant to test a
 rejection path, which needs its own operation schema rather than
 BorrowBook's?"]

That question is the actual payoff, not a rhetorical flourish. It distinguishes two mistakes that look identical from the outside — a scenario reporting an outcome the current implementation doesn’t produce — but need entirely different fixes: an operation modelled with the wrong precondition, versus a scenario silently testing a code path no schema was ever written to cover. A plain Given/When/Then runner can’t tell these apart; a schema, checked independently of any implementation, can.

A Fuller Worked Example: Two Operations and a Real Invariant Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

The second dropdown option scales the same idea up: three pieces of interacting state (books, borrowedBy, and a per-member loanCount), two operations (BorrowBook, ReturnBook), and a genuine cross-cutting invariant — no member may hold more than three books at once, a rule that isn’t derivable from the book-tracking half of the state at all. Run it and its seven scenarios exercise four of the five outcomes schema_check can return (ok, precondition_violated, invariant_violated_before, and postcondition_violated; the fifth, invariant_violated_after, has no scenario here): an available title accepted, a title someone else has out rejected, a member at the loan limit rejected, a corrupted loan record caught by the invariant before the operation is even considered, a scenario whose own claimed effect doesn’t match what its postcondition demands, and a clean return accepted and a spurious one rejected. Full source: self_hosting/examples/library_loans_schema_demo.patlang.

Beyond Hand-Written Scenarios: Synthesis Integration

A schema doesn’t only check scenarios a person wrote by hand. The same schema_check_values core also plugs into two of PatLang’s existing program-synthesis mechanisms as a stronger correctness oracle — catching an artifact that’s internally consistent with its own training data or its own plan, but still wrong by an independent standard. Both are in the example list at the top of the page and run there, in the browser; the output each one produces is printed below its description.

Inductive Synthesis: A Logically Valid Rule, Still Policy-Violating Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

BDD as Specification covers PatLang’s inductive-logic-programming engine deriving grandparent(X) :- parent(X,Y), parent(Y,Z) from training facts and examples. That derivation is provably correct with respect to its own training data — but the engine has no way to know about a constraint from a completely different part of a system, e.g. a policy that names specific people. self_hosting/lib/schema_synthesis_bridge.patlang asserts an already-induced rule into PatLang’s logic engine, enumerates every value it proves true, and checks each one against a schema. To run it here, choose “Inductive synthesis” in the example list at the top of the page. The engine tests each candidate rule in a clean interpreter created inside the page: interp_run compiles the test script and hands it to world_run. That host call swaps every global store the interpreter keeps (facts, rules, objects, virtual files, string and list handles) for an empty set, runs the script with its output captured, and puts the caller’s state back afterwards. Native PatLang uses the same call instead of spawning pat.exe, and falls back to a subprocess only when a wall-clock timeout or stdin is asked for.

  ok: induction succeeds on the training examples
  ok: induced rule is the expected 2-hop parent/parent chain
  ok: the induced rule is caught violating an unrelated schema policy
  ok: the flagged candidate is the restricted name, not the other one
tests: 4 passed, 0 failed
ALL TESTS PASSED

Two people, “alice” and “dave”, both satisfy the induced rule — the training data treats them identically. A GrandparentPolicy schema with an independent restricted-names list catches “dave” specifically, without touching the induction engine’s own logic at all. Full source: self_hosting/schema_synthesis_bridge_selftest.patlang.

GOAP Planning: Checking Real State, Not a Parsed Label Ephemeral / ToolingKnowledge that evolves in months to a year — check for updates

PatLang’s pre-existing GOAP contract system (goap_verify_contracts) can only check a contract against a string-parsed action-label binding, like extracting X=5 out of the text "scale(X=5)" — it has no way to express “and the book must not also still be at the origin branch,” because that needs the plan’s full resulting state, not one action’s own parameter. A new host function, plan_with_state, exposes that resulting state directly. It exists in three places: as a Rust interpreter host function, in the Rust-to-native codegen path (the one the in-page compiler is built from), and, canonically, as self-hosted PatLang in self_hosting/lib/x64_runtime.patlang, compiled and run through the patc1.exe --x64 production toolchain as well as the interpreter. Choose “GOAP: interlibrary transfer” in the example list at the top of the page to run it here.

  ok: the planner finds the full three-hop route
  ok: step 1 packs the book for transit
  ok: step 2 ships it to the depot
  ok: step 3 ships it on to the destination branch
  ok: the real resulting state has the book at branch_b
  ok: the real resulting state no longer has it at branch_a
  ok: the real resulting state has no dangling in-transit record
  ok: the full transfer plan satisfies the transfer policy
  ok: a destination with no shipping route is reported as no_plan_found
tests: 9 passed, 0 failed
ALL TESTS PASSED

A rare book moves from one branch to another through a three-step GOAP plan (pack for transit, ship to the depot, ship on to the destination); the schema checks the plan’s resulting facts — the book present at the destination and absent from the origin, not inferred from the last action’s own label text. A destination with no shipping route is correctly reported as no_plan_found, distinct from a schema violation. Full source: self_hosting/examples/interlibrary_transfer_goap_demo.patlang.

The Other Direction: Schema Suggesting Scenarios Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

Checking existing scenarios against a schema is the easier direction. The harder, more useful direction runs the other way: since a schema states a universally-quantified property rather than one instance, a schema-aware tool could enumerate concrete cases a scenario set doesn’t cover and propose them, rather than waiting for someone to think of the edge case by hand. This isn’t a new idea — it’s what property-based testing already does, generating concrete test cases from a stated property instead of a human enumerating them by hand3. This direction is now built, deterministically, with no LLM in the loop: given an operation, the generator searches the schema’s own reachable states and declared input domains — the same search the explorer already runs — for one state and input where the operation is enabled, and one per require clause where every other clause holds and that one alone fails. A clause with no such state, typically because it is implied by another or is tautological within its own declared domain, is reported rather than given an invented scenario.state the rule, generate the cases: cf. property-based testing

Every word the generator prints is either the schema author’s own text (a fact, then, or reject template, an operation or clause name) or a value taken from the state that was found and independently checked; nothing fills a gap in the schema’s own vocabulary. Run on the vending machine above, for BuyVM:

Feature: BuyVM (VendingMachine)
  Someone wants to buy a snack with money

Scenario: BuyVM succeeds
  When cookie is in stock
  And Bowen selects cookie
  Then BuyVM succeeds

Scenario: BuyVM is rejected: map_get_or(inventory, item, 0) > 0
  When Bowen selects chips
  Then the vending machine reports map_get_or(inventory, item, 0) > 0

Scenario: BuyVM is rejected: currentMoneyValue >= map_get(price, item)
  When cookie is in stock
  And Bowen selects cookie
  Then the vending machine reports currentMoneyValue >= map_get(price, item)

The third require clause, item in snacks, is reported separately rather than given a scenario: the operation’s own domain for item is snacks, so every value the search can try already satisfies it, and inventing a value outside that domain to violate it would not be a value the schema was ever checked against. Feeding this generated feature back through the same analysis that checks a hand-written one reports it consistent — the generator’s own witnesses hold up under the same check a person’s scenario would face, which is the actual test of whether generating them was worth doing.

From Examples to Every Reachable State Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

The mechanism above checks the states a scenario supplies. A second layer, written after reading Liu’s thesis, declares the schema as text and checks it against every state it can reach. It also runs from the command line. A declaration is a short block in an ASCII notation with sets, maps, quantifiers, and a trailing apostrophe for the after-state of a variable. An excerpt from the thesis’s vending machine, including the lines that say what each phrase in a scenario asserts:

schema VendingMachine
state inventory, currentMoneyValue
const snacks = set_of("cookie", "chocolate", "chips")
const price = map_of("cookie", 5, "chocolate", 7, "chips", 3)
const maxMoney = 20
init inventory = map_of("cookie", 2, "chocolate", 1, "chips", 0)
init currentMoneyValue = 0
domain item = snacks
invariant currentMoneyValue >= 0 and currentMoneyValue <= maxMoney

operation BuyVM(item)
  require item in snacks
  require map_get_or(inventory, item, 0) > 0
  require currentMoneyValue >= map_get(price, item)
  ensure currentMoneyValue' == currentMoneyValue - map_get(price, item)
  ensure inventory' == map_put(inventory, item, map_get(inventory, item) - 1)
end

fact {item} is in stock => map_get_or(inventory, item, 0) > 0
fact Bowen inserts {amount} dollars => currentMoneyValue > 0
fact Bowen selects {item} => item in snacks
goal buy a snack with money => BuyVM

Each clause is kept as a parsed tree instead of a compiled function, so a checker can read it: which clause failed, which state variables it mentions, and what the operation does to the state. Three checks follow.

Exploration. Starting from the initial state, the explorer applies every operation to every combination of values in the input domains the schema declares. It checks the invariants and postconditions in each state it reaches, and stops at a violation with the shortest sequence of operations that leads there. A LibraryLoans variant whose ReturnBook forgets to lower a member’s loan count is caught after two steps, a borrow and a return:the shortest trace is the smallest counterexample

ReturnBook reaches a state that breaks an invariant: forall m in dom(loanCount) : map_get(loanCount, m) == map_count_val(borrowedBy, m)
  step 1: BorrowBook with {"Dune", "A. Diallo"}
  step 2: ReturnBook with {"Dune"}

A person would have to write the scenario that reaches that state. The explorer needs none. Exhaustive here means every state reachable through the declared domains and no more, and the result says so when a search stops at its bound before finishing.

The feature check. The property in Liu’s process is that in every state where the predicates derived from a scenario’s Given and When clauses do not all hold, the goal-related operation is not enabled2. The fact and goal lines above are the analyst’s part, and the explorer’s states supply the “every state”. On listing 15 of the thesis the vending machine comes back consistent:

Goal: buy a snack with money  (goal-related operation: BuyVM)
Schema states explored: 126, exhaustive: true
Scenario (positive): Buying a cookie using money when the cookie is in stock
    realisable: reached by 1 step(s), then the operation runs with {"cookie"}
    outcome not checked, no meaning is declared for: the vending machine dispenses a cookie
Consistent: every fact is enforced by BuyVM, and each scenario holds when the schema runs it.

Remove the requirement that enough money has been inserted, and clamp the balance at zero so the schema stays internally consistent, and the check reports the missing requirement with the state where it matters. Here that is the initial state, where a snack can be bought with no money inserted:

Requirement missing from the schema: "Bowen inserts {amount} dollars" (currentMoneyValue > 0)
    BuyVM is enabled with inputs {"cookie"} in a state reached by 0 step(s), where that fact is false
Inconsistent: the feature and the schema disagree.

The Then step of the same scenario — “the vending machine dispenses a cookie” — is reported too, in both runs: outcome not checked, no meaning is declared for: the vending machine dispenses a cookie. Nothing in the schema says what dispensing means, so the claim is neither confirmed nor contradicted; it is named as unchecked rather than passed over in silence.

Realisability. The line beginning “realisable” comes from a check that is our own addition to Liu’s. Each positive scenario needs some reachable state that satisfies its facts and lets the operation run. A scenario that no reachable state satisfies, or one whose facts hold in reachable states where the operation never runs, is reported as such.

The property checked is Liu’s. Checking it by exploring the states of a schema declared in PatLang, the realisability check, and the refusal to analyse a schema that breaks its own invariants are our additions. Two limits carry over or are new. An ensure clause of the form a' == expr defines how a variable changes, and a variable with no such clause is taken as unchanged, which is a stronger reading than Z’s. A postcondition that only constrains a variable, such as n' > n, leaves the after-state open, and the schema is refused instead of explored on a guess.

Outcomes, Negative Scenarios, and Sequences

Three things the thesis leaves out2 are checked here, each by running the schema rather than trusting a scenario’s own arithmetic.

Outcomes. A then template => expr line states what a phrase claims about an operation’s result, in terms of the before-state, the after-state (primed), and the phrase’s own captures. Rather than comparing a scenario’s claimed after-state to the schema’s postcondition — which only catches a claim the postcondition itself disagrees with — the schema now computes the after-state by running the operation, and the claim is checked against what was actually computed. A claim that matches how a person hand-writing the scenario got the arithmetic wrong, but wrote a postcondition that happens to agree, is caught here where it was not before.

Negative scenarios. A Then phrase matching a negative or reject declaration marks a scenario as a rejection. It is no longer skipped: some reachable state must satisfy the scenario’s facts and disable the goal operation, and a reject phrase names the exact require clause expected to be the one that fails. A rejection blamed on the wrong clause, or one the schema never actually makes, is reported by name.

Sequences. A do template => Operation(arg, ...) line lets a When phrase run an operation instead of only asserting a fact about it. A scenario built from these is executed from every reachable state that satisfies its Given facts, one step at a time, checking each then claim against the state that step actually produced. The order events happen in is checked by happening, not modelled separately.

Refinement FoundationalKnowledge that endures for decades — core principles

Liu’s thesis raises, and leaves open, whether consistency between a behavioural specification and a Z specification survives the Z specification’s own refinement2. A concrete schema here can declare refines Abstract and one retrieve line per abstract state variable, defining it in terms of the concrete state. The check is the standard forward-simulation obligation, run over every state the concrete schema reaches: the concrete initial state retrieves to the abstract one, every retrieved state satisfies the abstract invariants, the concrete operation is enabled wherever the abstract one is (it may be enabled more often — weakening a precondition is a valid refinement), and where both are enabled, the retrieved concrete outcome equals the abstract one. A LibraryLoans variant that adds a maintained loan count refines the simple schema; the same variant with a three-loan limit added does not, and is reported with the operation, the clause that refuses it, and the trace to the state where it matters.

Once a refinement is confirmed, a feature already checked against the abstract schema can be checked against the concrete one, with each abstract fact and outcome read through the retrieve function. A concrete vending machine that adds a sales counter, correctly refining the original, keeps the feature consistent. The same concrete machine with the money-check weakened is still a valid refinement — weakening a precondition always is — but the feature is no longer consistent with it, and the missing requirement is reported by name. Confirming the refinement and confirming the feature survives it are two different checks, run separately, because the first says nothing about the second.

Inferring a Schema from a Feature Ephemeral / ToolingKnowledge that evolves in months to a year — check for updates

The boundary this section describes, stated first in the same Given/When/Then shape a feature file itself uses — a summary of the capability rather than a scenario to check, so it is shown, not run:

Feature: What BDD-to-Z inference can and cannot do

  Scenario: Vocabulary alone
    Given a feature that quotes or numbers the values that vary between scenarios
    When it is read by zi_infer_skeleton
    Then fact, do and then templates are inferred
    But require and ensure stay the placeholder true

  Scenario: A closed vocabulary of quantities and arithmetic
    Given a feature whose Given and Then lines also say things like "contains at least N X" or "'s balance is decreased by N"
    When it is read by zi_infer_skeleton_auto
    Then the state variables those phrases name, and real require/ensure clauses for them, are inferred too

  Scenario: Ordinary prose is never guessed at
    Given a feature with no recognised phrasing, however carefully written
    When it is read by either function
    Then no state variable, and no require or ensure clause, is invented for it
    And the phrase is left exactly as a vacuous fact or then line, unchanged

  Scenario: What is never inferred, whatever the feature says
    Given any feature, however precisely its scenarios are written
    When it is read by zi_infer_skeleton or zi_infer_skeleton_auto
    Then no init value and no operation input domain is ever produced
    And the skeleton is refused when explored, not guessed into running

  Scenario: Induction proposes, it never asserts
    Given a schema whose facts are already filled in, and states classed accepted or rejected
    When zi_suggest_requires runs
    Then an already-declared fact that discriminates between them is proposed as a candidate require clause
    But it is never written into the schema, or treated as checked, automatically

The direction above assumes a schema already exists. Often it doesn’t: a project accumulates Gherkin scenarios first, and the formal side never gets written. zi_infer_skeleton reads the vocabulary out of a feature and writes a schema skeleton from it, reversing the same quoting convention the fact/then/do templates above already use: a quoted span or a bare number in a Given/When/Then line generalises to a placeholder, and plain unquoted word variation does not, since deciding that “cookie is in stock” and “chips are in stock” share a template is a judgement a person has to make, not a pattern a parser can find. Given and Then lines become fact and then templates. A scenario’s When line, together with any And/But that follow it, is joined into one combined action before being generalised, so a feature that spreads one operation’s inputs across several lines — as the thesis’s own vending-machine scenario does — still infers one action of the right arity rather than several mismatched ones.

What the skeleton cannot contain is anything Gherkin text doesn’t say: no state variable, no domain, no real precondition or effect. The skeleton declares none of those, states its operation’s require and ensure clauses as the placeholder true, and leaves a TODO comment where a person’s judgement is needed, rather than guessing at any of it. It is still real, loadable PatLang the moment it is written — zs_load accepts it — because a vacuous clause and a missing declaration are both syntactically complete, only semantically empty. Run on the thesis’s own vending-machine feature, with no hand-written schema anywhere in the loop:

Output (click to expand)
schema BuyASnackWithMoneySchema
# TODO: this schema has no state yet -- Gherkin text names no
# state model, so none was guessed at. Add one, e.g.:
#   state someVariable
#   init someVariable = ...

operation BuyASnackWithMoney(p1)
  # TODO: replace with the real precondition(s) for BuyASnackWithMoney.
  require true
  # TODO: replace with the real effect(s)/postcondition(s).
  ensure true
end

fact cookie is in stock => true

do Bowen inserts {p1} dollars and Bowen selects cookie => BuyASnackWithMoney(p1)

then the vending machine dispenses a cookie => true

goal buy a snack with money => BuyASnackWithMoney

--- checking that the skeleton is valid, loadable PatLang ---
Loads cleanly as schema BuyASnackWithMoneySchema. Its require/ensure clauses are still the placeholder "true" above -- add real state, domains and clauses before exploring it.

Comparing this against the hand-written VendingMachine schema shown earlier makes the design’s real boundary visible. Its author judged that both the dollar amount and the item name vary between scenarios, writing Bowen inserts {amount} dollars and Bowen selects {item}. The inferred skeleton catches the dollar amount, a bare number, as Bowen inserts {p1} dollars. It leaves cookie as fixed text, because the feature never quotes it and never writes a second scenario that selects a different snack — nothing in the wording signals that the word varies. A feature that does vary an unquoted value across scenarios still needs a person to notice and generalise it by hand. Exploring the skeleton as it stands reports missing_domain rather than a state count: the same honest refusal a hand-written schema with no declared domain gets, not a failure specific to inference.

What the skeleton cannot contain, above, is anything Gherkin text doesn’t say — but “doesn’t say” has its own boundary. A schema’s require/ensure clauses stay the placeholder true because free English carries no fixed formal meaning: “the cookie is nice” and “the cookie is in stock” are indistinguishable to a parser. A small, closed table of quantity and arithmetic phrasings is a different case — “contains at least N X”, “’s balance is decreased by N”, and a handful of others each have one fixed, unambiguous formal meaning, the same way a quoted span or a bare number does. zi_match_require/zi_match_ensure recognise exactly those phrasings, and only ever produce a clause when the phrase’s own subject or field literally names one of the schema’s already-declared state variables — never against arbitrary prose, and never by guessing which variable was meant.

A feature written this precisely has largely already written the formal clause in English, so this is closer to compiling a small controlled vocabulary than to reading arbitrary BDD — a real capability, conditional on that discipline, not a general upgrade to Phase 1’s own guarantee. Naming what three of the original scenario’s phrases assert, rather than leaving them as plain facts:

    And vending machine inventory contains at least one cookie
    And Bowen's balance is at least 10 dollars
    ...
    And the vending machine inventory subtracts a cookie
    And Bowen's balance is decreased by 10 dollars

gives real preconditions and effects, and infers the state line itself through the same table — read for the variable’s name rather than for a clause. zi_infer_state_vars proposes inventory because a require-shaped phrase names it and balance because a scalar one does, never from an unrelated noun like the item or the actor; zi_infer_skeleton_auto chains state inference and clause inference together, so nothing below was supplied by hand beyond the feature’s own text:

Output (click to expand)
schema BuyASnackWithMoneySchema
state inventory, balance
# TODO: no phrase in the feature says what these start at.
#   init inventory = ...

operation BuyASnackWithMoney(p1)
  require map_get_or(inventory, "cookie", 0) >= 1
  require balance >= 10
  ensure inventory' == map_put(inventory, "cookie", map_get(inventory, "cookie") - 1)
  ensure balance' == balance - 10
end

fact cookie is in stock => true
fact vending machine inventory contains at least one cookie => true
fact Bowen's balance is at least {p1} dollars => true

do Bowen inserts {p1} dollars and Bowen selects cookie => BuyASnackWithMoney(p1)

then the vending machine dispenses a cookie => true
then the vending machine inventory subtracts a cookie => true
then Bowen's balance is decreased by {p1} dollars => true

goal buy a snack with money => BuyASnackWithMoney

--- checking that the skeleton is valid, loadable PatLang ---
Loads cleanly as schema BuyASnackWithMoneySchema. State (inventory, balance) and the require/ensure clauses above came from the feature's own wording -- add init values and an input domain before exploring it.

A feature with no recognised phrase at all — the plain version run earlier — gets Phase 1’s output back completely unchanged, confirmed by a regression test rather than left to assumption. Hand-completing this skeleton with init values and a domain for p1 (still nobody’s job but a person’s: no phrase says what a snack machine starts with, or what amounts a buyer might insert) makes it explorable: two reachable states, one transition, a cookie bought.

A second, bounded step goes further, but only once a person has filled a schema’s facts in with real meaning. For an operation with some scenarios classed as accepted and others rejected, zi_suggest_requires proposes an already-declared fact as a candidate require clause whenever it holds in every accepted state and fails in at least one rejected one. It searches nothing beyond the vocabulary already written down — this is not expression synthesis — and every result carries its own support and counter-example counts rather than being asserted as checked:

require amount is small  (holds in 2/2 accepted states; excludes 1/1 rejected states)

A fact merely correlating with acceptance is not the same claim as a fact a schema’s author intended as a precondition, so a suggestion here is exactly that: a hypothesis for a person to confirm, or reject, before it becomes a require clause the schema is actually checked against. Deriving accepted and rejected states automatically from a checked feature, rather than supplying them by hand as above, is the natural next integration and isn’t built yet. Full source: self_hosting/lib/zs_infer.patlang. The generated examples above are checked into self_hosting/examples/zs/vending_machine_inferred.zschema and self_hosting/examples/zs/priced_vending_machine_inferred.zschema, each alongside the feature it came from.

Program Flow Ephemeral / ToolingKnowledge that evolves in months to a year — check for updates

A declaration is loaded once and kept as parsed clauses. The explorer, the feature analysis, the generator, and the refinement check all read from that same entry.

flowchart TD accTitle: Program flow of the declared-schema layer accDescr: A schema text is loaded and parsed into clauses. The explorer searches its reachable states and reports a violation with the shortest trace, or a clean result. A feature text is parsed, its steps are matched to facts declared in the schema, and the analysis checks each scenario for realisability and each fact for necessity over the explored states. A feature text can also, without any schema, be read by zi_infer_skeleton_auto into a schema skeleton: vocabulary becomes fact, do and then templates always; state variables and their require and ensure clauses become real wherever the feature names them through a closed table of quantity and arithmetic phrasings, and stay a placeholder otherwise, ready for a person to fill in. S["Schema text
state, invariants, operations"] --> L["zs_load
parse each clause into a tree"] L --> R[("Registry entry")] R --> E["zs_explore
breadth-first search of reachable states"] E -->|"invariant or postcondition broken"| V["Violation:
shortest sequence of operations"] E -->|"every state checked"| OK["ok, or ok_bounded
if the state limit was hit"] F["Feature text
Given / When / Then"] --> FP["zf_parse_feature
goal, scenarios, steps"] FP --> MF["match each step to a fact
declared in the schema"] R --> MF E -->|"reachable states"| AN MF --> AN["zs_analyse_feature
outcomes, negative scenarios,
sequences, realisability, necessity"] AN --> RES["consistent or inconsistent,
with findings"] R --> GEN["zs_generate_feature
one scenario per witnessed clause"] GEN -.->|"fed back in"| F R --> REF["zs_refines
forward-simulation obligations"] REF --> RRES["a concrete schema either
refines the abstract one, or doesn't"] F --> INF["zi_infer_skeleton_auto
vocabulary, plus a closed table of
quantity/arithmetic phrasings"] INF --> SK[("Schema skeleton
state and require/ensure are real where a
phrase names them, else placeholder true")] SK -.->|"a person adds init values,
an input domain, and any
clause still a placeholder"| L style V fill:#F5ECDB style RES fill:#E8F5E9 style RRES fill:#E8F5E9 style SK fill:#F5ECDB

Inside the explorer, each state is expanded by trying every operation with every combination of the declared input values. A clock, not a state count, decides when the search reports progress, so a state with thousands of transitions cannot delay a report.

flowchart TD accTitle: The explorer's search loop accDescr: Starting from the initial state, the explorer takes each queued state, tries every operation with every combination of declared input values, skips those whose require clauses fail, computes the after-state, stops with a trace if a clause or invariant fails, and queues states it has not seen. A clock-driven tick reports progress and can stop the search. I["initial state"] --> Q["queue of states"] Q --> N["take the next state"] N --> OP["next operation with
next combination of inputs"] OP --> PRE{"all require
clauses hold?"} PRE -->|no| OP PRE -->|yes| EFF["compute the after-state
from the ensure equations"] EFF --> CHK{"ensure clauses and
invariants hold?"} CHK -->|no| BAD["stop and report
the trace to this step"] CHK -->|yes| SEEN{"state already seen?
canonical key"} SEEN -->|yes| OP SEEN -->|no| ADD["queue it and record
the step that reached it"] ADD --> OP OP -->|"all combinations tried"| Q Q -->|"queue empty"| DONE["every reachable state checked"] T["clock tick, every 120 ms
progress line, status, quit"] -.-> OP style BAD fill:#F5ECDB style DONE fill:#E8F5E9

Try It

The panel below runs the same libraries in this page, in a background worker so the page stays responsive. Beyond exploring a schema and checking a feature against it, the dropdown includes an outcome-checking example, a negative scenario, a multi-step sequence, the schema-to-Gherkin generator, a data refinement, and inferring a schema skeleton (including real preconditions, effects and state, where the feature names them precisely enough) from a feature with no schema at all — each run with the same code as the command-line tools. Edit the schema or the feature and run it again; Cancel stops the worker.

(not run yet)

Timings Ephemeral / ToolingKnowledge that evolves in months to a year — check for updates

Times are wall-clock milliseconds or seconds on one Windows 11 machine, taken as the median of three runs unless a row says otherwise. The native column is the project’s pat.exe interpreter, one fresh process per run, and includes reading the libraries. The browser column is headless Chrome running the page’s own WebAssembly interpreter in a background worker, and includes starting the run.

Live exampleSearchNative interpreterIn the browser
LibraryLoans, a return that forgets to lower the countviolation found at step 20.04 s0.71 s
LibraryLoans, correct44 states, 186 transitions0.10 s0.77 s
Vending machine against listing 15126 states, 388 transitions0.16 s0.83 s
Vending machine that sells with no money126 states, 388 transitions0.14 s0.83 s
LibraryLoans, six titles668 states, 5,052 transitions2.17 s3.14 s

The small examples cost almost the same in the browser whatever they search. A trivial program starts there in about 3 ms, and the 82 KB of libraries with nothing to search takes 0.65 s: reading the libraries is most of every small browser figure. The native interpreter reads them in 0.03 s. Setting that fixed cost aside, the six-title search took 2.49 s in the browser against 2.14 s natively.

How the cost grows was measured on the native interpreter with LibraryLoans at three to seven titles and two members. Time per transition rose by about 33 percent while the state space grew 35-fold:

TitlesStatesTransitionsTimePer transition
3441860.06 s333 µs
41106000.22 s370 µs
52741,8000.69 s382 µs
66685,0522.10 s415 µs
71,55813,0625.80 s444 µs

The rise follows the size of each state. A control with a single integer of state, so that a state stays the same size while the number of states doubles, keeps its cost per transition between 34 and 36 µs across a 16-fold increase in states:

StatesTransitionsTimePer transition
50150018 ms36 µs
1,0011,00034 ms34 µs
2,0012,00068 ms34 µs
4,0014,000140 ms35 µs
8,0018,000282 ms35 µs

At nine titles and two members the search covers 7,060 states and 67,140 transitions. Exploring alone took 34 s, and checking a three-fact feature against the explored states took 51 s in total (single runs, native interpreter). Status queries sent to the command-line driver during the exploration came back in 23 to 68 ms each, including the time to start the second process that sent them.each extra title multiplies the states

Open Questions and Limits Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

The checking direction — does this one scenario satisfy the schema — is cheap: substitute concrete values into a predicate and evaluate it, confirmed directly by every example on this page running well under the length of a page load. The harder question — does a feature’s full set of scenarios, taken together across a whole sequence of operations, ever drive the state into something the invariant forbids — is a state-space exploration problem, not a per-scenario evaluation, and it inherits exactly the scaling limit Formal Methods already names for Z on its own: a schema doesn’t check itself past a certain size without tool support. Liu’s process hands that problem to the ProB model checker2. The declared-schema layer takes it on directly, and its cost grows with the state space. The time per transition rose by about a third while the number of states grew thirty-fivefold, and stayed roughly flat when the size of each state was held constant, so the growth comes from each state getting larger and not from the number of states seen so far. A narrower, now-resolved limit: an absence-sentinel ambiguity in pmap_get (a missing key and a genuinely falsy stored value both read back the same way) is a documented hard rule — pmap_has is the only authoritative presence check — rather than a live bug, since every schema built so far uses string- or list-typed state where it doesn’t bite.

References

  1. Liu, B. (2019). Using behavioural specifications to support model-checking [Master’s thesis, University of Waikato]. https://hdl.handle.net/10289/13028 ↩

  2. Liu, B. (2024). Integrating behavioural and formal specifications [PhD thesis, University of Waikato]. https://hdl.handle.net/10289/17330 ↩ ↩ ↩ ↩ ↩ ↩ ↩ ↩ ↩

  3. Shao, L. (2025). Test generation from Z specifications using LLM support for web system [Unpublished dissertation, University of Waikato]. Supervised by Judy Bowen; shared with the author by Bowen. Not listed in the university’s research repository at the time of writing.

  4. Claessen, K., & Hughes, J. (2000). QuickCheck: A lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices, 35(9), 268–279. https://doi.org/10.1145/357766.351266 ↩