Schemas and Scenarios: A Speculative Z/BDD Hybrid

FormalFormal 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. Those two pages develop each idea on its own; this one asks what sits between them — a single specification artifact where 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. Nothing below is built. No PatLang parser extension, host function, or checker described past this point exists yet — what follows is a design sketch, not documentation of a shipped feature.

Prior Art

ThisThis isn't unclaimed territory, and it would be dishonest to write about it as though it were. 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 models¹; the follow-on PhD work, supervised by Judy Bowen, Jessica Turner, and Steve Reeves, does the same specifically against Z specifications, including checking that the consistency survives a Z specification's own refinement steps — the harder, more general version of the same problem, aimed at safety-critical interactive systems².

What follows differs in scope, not in the underlying idea. Liu and Bowen's work treats the behavioural specification and the Z specification as two separate documents, reconciled by an external consistency checker — a defensible choice for safety-critical systems where a formal model and a requirements document may genuinely come from different processes. The sketch below instead asks what the same idea looks like folded into one language and one executable artifact: PatLang already writes contracts (require/ensure) as And clauses inside Given/Then, per BDD as Specification's account of the split between what a scenario claims and what a contract guarantees. A schema is, structurally, a contract generalised across every operation touching one piece of state rather than pinned to a single function call — connecting that generalisation to PatLang's own scenario-plus-contract convention, in one file rather than two, is the specific extension explored here. The schema/scenario pairing itself is Liu and Bowen's.

Two Kinds of Claim, Briefly

AA Z schema states what must hold for every input satisfying its precondition — Formal Methods' 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.

A Worked Sketch

ReusingReusing BorrowBook's schema from Formal Methods and the library domain from Relational Modelling, here is what attaching that schema to a feature file might look like, as a speculative extension of PatLang's existing Feature:/Scenario: syntax. None of the new keywords below (Schema:, Operation:, the Set<T>/Map<K,V> types) exist in PatLang today:

Feature: Library loans

  Schema: LibraryLoans
    state:
      books      : Set<Title>
      borrowedBy : Map<Title, Member>
    invariant:
      keys(borrowedBy) subset_of books

  Operation: BorrowBook
    inputs: title, member
    require: title in books
    require: title not in keys(borrowedBy)
    ensure:  borrowedBy' == borrowedBy with [title -> member]

  Scenario: Borrowing an available book
    Given the library holds "Dune"
    And "Dune" is not currently borrowed
    When "A. Diallo" borrows "Dune"
    Then "Dune" is borrowed by "A. Diallo"

A schema-aware checker's job here is different from what PatLang's actual BDD runner does today. Today, a scenario is checked against a real implementation: run the code, compare Then to the actual result. A schema adds a second, independent check that needs no implementation at all — do this scenario's own Given/When/Then values satisfy BorrowBook's stated require and ensure clauses? The scenario above does: "Dune" is in books, not yet in borrowedBy, and Then matches what ensure predicts once title and member are substituted in.

The more interesting case is a scenario that shouldn't pass:

  Scenario: Borrowing an already-borrowed book
    Given the library holds "Dune"
    And "Dune" is currently borrowed by "S. Okonkwo"
    When "A. Diallo" borrows "Dune"
    Then the system rejects the request

Checked against BorrowBook's schema rather than run against any code, this scenario fails before implementation ever enters the picture — its own Given already violates BorrowBook's second require clause. That's not necessarily a mistake in the scenario; it's a mismatch between which operation the scenario is actually testing and which schema it's being checked against. A schema-aware checker, in PatLang's existing style — the same tagged-diagnosis-plus-question pattern BDD as Specification's induction engine already uses for a scenario a rule can't satisfy — could say so directly rather than just reporting a mismatch:

> schema_check("Borrowing an already-borrowed book", BorrowBook)
["require_violated", ["title not in keys(borrowedBy)"]]

> question
"This scenario's Given already has \"Dune\" present in borrowedBy, which
 violates BorrowBook's own require clause before the operation runs. Is this
 scenario meant to test the rejection path -- in which case it needs its own
 operation schema for that path, not BorrowBook's -- or is BorrowBook's
 precondition wrong?"

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.

The Other Direction: Schema Suggesting Scenarios

CheckingChecking 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 in principle enumerate concrete cases the current scenario set doesn't cover and propose them as new scenarios, rather than waiting for someone to think of the edge case by hand. This isn't a new idea either — it's what property-based testing already does, generating concrete test cases from a stated property instead of a human enumerating them by hand³. Applied here, a generator reading BorrowBook's schema could propose the boundary case neither scenario above reaches — borrowing the last unborrowed copy of a title every other copy of which is already out — the kind of case a schema states implicitly (nothing in the invariant treats "last copy" specially) but a hand-written scenario set easily forgets to exercise. It's the same gap-finding instinct BDD as Specification's induction engine already applies in the opposite direction — there, diagnosing which scenario a rule set's evidence fails to distinguish; here, diagnosing which case a schema permits that no scenario has yet exercised.

What Would Actually Be Needed

TurningTurning this from a sketch into something runnable needs several pieces of new machinery, none of which exist today:

Piece	Status today
Feature:/Scenario:/Given/When/Then	Real, existing PatLang syntax
require/ensure contracts	Real, existing PatLang syntax — but scoped to one function call's scalar arguments
Schema:/Operation: blocks	Does not exist
Set<T>/Map<K,V> state types	Does not exist
Given/When/Then → schema-variable binding	Does not exist
Predicate evaluator over set/map state	Does not exist
Schema-to-scenario generator	Does not exist

The binding layer is the least obvious of these and the easiest to underestimate: translating a scenario's concrete strings into instantiations of a schema's typed state variables — "the library holds "Dune"" becoming books ∪= {"Dune"} — isn't free. It needs an explicit convention for which phrasing maps to which state update, and nothing like that exists for PatLang's BDD parser today; without it, a schema-aware checker has no way to know what a sentence in a Given clause is actually claiming about the state. The predicate evaluator is a smaller step from what already exists — PatLang's contract mechanism already evaluates require/ensure clauses, just not ones that quantify over a whole set or map rather than a single call's scalar arguments. The generator, by contrast, is a materially larger undertaking than everything else on this list: checking a given scenario against a schema is evaluation; generating a scenario a schema doesn't yet have is search, over a typed value space that would need its own enumeration or constraint-solving strategy.

Open Questions and Limits

TheThe checking direction — does this one scenario satisfy the schema — is cheap: substitute concrete values into a predicate and evaluate it. 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. Adding scenarios into the mix doesn't remove that limit; it adds a second artifact that has to stay consistent with the first, across every change to either one. That's precisely the harder problem Liu and Bowen's PhD work spends its own length on, under Z refinement specifically, rather than something a short design sketch resolves in passing.

References