Schemas and Scenarios: A Working 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. 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.

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. What’s built here instead folds the same idea into one language and one executable artifact: PatLang schemas and scenarios live in the same source, checked by the same tool, in one pass. 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 — 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.

From Sketch to Implementation: What Changed

AnAn earlier version of this page sketched a Schema:/Operation: block extension to PatLang’s Feature-file syntax, with require/ensure clauses written as inline text. Building it for real, rather than just imagining it, forced two corrections — both found by reading the actual PatLang source rather than trusting the sketch’s own assumptions:

• require/ensure/assert are fatal on violation — confirmed directly in rust-runtime/src/ir/hosts.rs: a failed contract check aborts the running program. That rules out the sketch’s inline text clauses outright; a schema check has to report a diagnosis and keep running, not kill the process on the first violation. The real implementation represents a schema’s invariant, precondition, and postcondition as ordinary, separately-compiled PatLang functions returning bool, invoked by name through PatLang’s existing apply() primitive — the same mechanism self_hosting/lib/primitive_registry.patlang already uses for named contract predicates elsewhere in the codebase, not new machinery.
• apply() has no argument-spread form. A checking function written once, generic over any schema’s own number of state variables, can’t pass one positional argument per variable — it has no way to know in advance how many there’ll be. State and inputs are therefore always bundled as a single list argument: invariant_fn(state_list), require_fn(state_list, input_list), ensure_fn(before_list, after_list, input_list).

Set and Map types didn’t exist either, as the sketch already suspected — self_hosting/lib/pset.patlang and pmap.patlang are new, small, association-list-based libraries built to fill exactly that gap, following the same list-plus-linear-scan idiom already used elsewhere in the codebase rather than inventing a new primitive.

Try It Yourself: The Mechanism, Live

BothBoth 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). Pick an example from the dropdown, edit it if you like, and press Run.

Load example: LibraryLoans: one operation, one violation LibraryLoans: three operations, a real invariant

# =============================================================================
# Test framework (Stage 1 dialect): unit assertions plus a Gherkin-style
# feature runner. Step definitions are registered in the object store keyed
# by their text; features are plain text dispatched line by line, so the
# same framework covers unit, integration, and behaviour tests.
# =============================================================================

make a function called t_init returns done
  set_var("t_pass", 0)
  set_var("t_fail", 0)
  set_var("t_tagfilter", "")
  set_var("t_pending_tags", "")
  set_var("t_skipping", 0)
  return true
end

make a function called contains_text takes hay, needle returns r
  if needle.length > hay.length then
    return false
  end
  let i = 0
  while i <= hay.length - needle.length do
    if substr(hay, i, needle.length) == needle then
      return true
    end
    let i = i + 1
  end
  return false
end

make a function called check takes label, actual, expected returns ok
  if actual == expected then
    set_var("t_pass", get("__vars", "t_pass") + 1)
    print("  ok: " + label)
    return true
  else
    set_var("t_fail", get("__vars", "t_fail") + 1)
    print("  FAIL: " + label + " (got " + actual + ", want " + expected + ")")
    return false
  end
end

make a function called t_report returns ok
  let p = get("__vars", "t_pass")
  let f = get("__vars", "t_fail")
  print("tests: " + p + " passed, " + f + " failed")
  if f == 0 then
    print("ALL TESTS PASSED")
    return true
  else
    print("TESTS FAILED")
    return false
  end
end

# ---- Gherkin runner ----

# Register a step: step("a fresh till", "st_fresh_till")
make a function called step takes text, fname returns done
  new("Step", text)
  send(text, "set", "fn", fname)
  return true
end

make a function called starts_with takes s, prefix returns r
  if s.length < prefix.length then
    return false
  end
  return substr(s, 0, prefix.length) == prefix
end

make a function called trim_left takes s returns out
  let i = 0
  let scanning = true
  while (i < s.length) and scanning do
    let c = char_code(s, i)
    if (c == 32) or (c == 9) then
      let i = i + 1
    else
      let scanning = false
    end
  end
  return substr(s, i, s.length - i)
end

# Strip a Gherkin keyword; returns the step text or "" if not a step line
make a function called step_text takes line returns out
  if starts_with(line, "Given ") then
    return substr(line, 6, line.length - 6)
  end
  if starts_with(line, "When ") then
    return substr(line, 5, line.length - 5)
  end
  if starts_with(line, "Then ") then
    return substr(line, 5, line.length - 5)
  end
  if starts_with(line, "And ") then
    return substr(line, 4, line.length - 4)
  end
  return ""
end

# Run only scenarios whose preceding @tag line contains `tag` ("" = all)
make a function called run_feature_tagged takes feature, tag returns ok
  set_var("t_tagfilter", tag)
  return run_feature(feature)
end

make a function called run_feature_file takes path returns ok
  return run_feature(read_file(path))
end

make a function called run_feature takes feature returns ok
  let h = str_intern(feature)
  let n = sc_len(h)
  let i = 0
  let line = sb_new()
  while i <= n do
    let c = sc_code(h, i)
    if (c == 10) or (c == -1) then
      let raw = trim_left(sb_str(line))
      let line = sb_new()
      if starts_with(raw, "@") then
        set_var("t_pending_tags", raw)
      end
      if starts_with(raw, "Feature:") then
        print(raw)
      end
      if starts_with(raw, "Scenario:") then
        let filter = get("__vars", "t_tagfilter")
        let tags = get("__vars", "t_pending_tags")
        set_var("t_pending_tags", "")
        if filter then
          if tags then
            if contains_text(tags, filter) then
              set_var("t_skipping", 0)
              print(raw + "  [" + tags + "]")
            else
              set_var("t_skipping", 1)
              print(raw + "  [skipped: needs " + filter + "]")
            end
          else
            set_var("t_skipping", 1)
            print(raw + "  [skipped: needs " + filter + "]")
          end
        else
          set_var("t_skipping", 0)
          print(raw)
        end
      else
        let text = step_text(raw)
        if (text != "") and (get("__vars", "t_skipping") != 1) then
          if starts_with(text, "require ") then
            handle_contract_step("require", substr(text, 8, text.length - 8))
          else
            if starts_with(text, "ensure ") then
              handle_contract_step("ensure", substr(text, 7, text.length - 7))
            else
              let fname = get(text, "fn")
              if fname then
                apply(fname)
              else
                set_var("t_fail", get("__vars", "t_fail") + 1)
                print("  FAIL: undefined step: " + text)
              end
            end
          end
        end
      end
      let i = i + 1
    else
      if c == 13 then
        let i = i + 1
      else
        sb_push(line, sc_char(h, i))
        let i = i + 1
      end
    end
  end
  return true
end

# =============================================================================
# pset: a minimal Set<T> built on a plain list with linear-scan membership,
# the same idiom already used by depgraph_list_contains and
# synth5_list_contains (self_hosting/lib/depgraph.patlang,
# self_hosting/lib/synthesis_lgg.patlang) rather than a new primitive --
# PatLang has no native Set type.
#
# Functional / return-new-collection style throughout (mirrors list_push's
# own semantics): every mutating-sounding operation returns a NEW list
# rather than mutating in place. This matters specifically for schema_bdd's
# before/after snapshotting, which needs an independent copy of state at
# two points in time -- an in-place structure would make "before" silently
# turn into "after" once the operation runs.
# =============================================================================

make a function called pset_new returns s
  return []
end

make a function called pset_contains takes s, item returns found
  let i = 0
  let n = to_num(list_len(s))
  while i < n do
    if s[i] == item then
      return true
    end
    let i = i + 1
  end
  return false
end

make a function called pset_add takes s, item returns s2
  if pset_contains(s, item) then
    return s
  end
  return list_push(s, item)
end

make a function called pset_remove takes s, item returns s2
  let out = []
  let i = 0
  let n = to_num(list_len(s))
  while i < n do
    if s[i] != item then
      let out = list_push(out, s[i])
    end
    let i = i + 1
  end
  return out
end

make a function called pset_size takes s returns n
  return to_num(list_len(s))
end

# Identity -- exposed so callers iterating a set's members don't need to
# know it's "just a list" internally; the name documents intent at the
# call site instead.
make a function called pset_to_list takes s returns items
  return s
end

# Set equality: same size, and every member of a is in b. Given pset_add's
# own dedup, equal size plus one-directional containment implies the
# reverse containment too (no way for b to hold something a doesn't
# without differing in size).
make a function called pset_equal takes a, b returns eq
  if pset_size(a) != pset_size(b) then
    return false
  end
  let i = 0
  let n = to_num(list_len(a))
  while i < n do
    if pset_contains(b, a[i]) == false then
      return false
    end
    let i = i + 1
  end
  return true
end

# =============================================================================
# pmap: a minimal Map<K,V> as an association list of [key, value] pairs with
# linear-scan lookup -- the exact same idiom already proven in
# self_hosting/lib/depgraph.patlang's depgraph_map_get/depgraph_map_append
# (a file->list-of-files map), generalised here to an arbitrary value type
# and given a full put/get/has/remove/keys surface. PatLang has no native
# Map/Dict type usable from self-hosted code at this scale.
#
# Functional / return-new-collection style throughout, for the same reason
# as pset.patlang: schema_bdd needs an independent before/after snapshot of
# state, which an in-place-mutating map wouldn't give for free.
#
# pmap_get returns [] (an empty list) for a missing key -- the same
# not-found sentinel depgraph_map_get already uses, not a distinct "Unit"
# literal (PatLang's dialect has no source-level Unit/nil literal to write
# directly). This is INHERENTLY AMBIGUOUS if a real stored value could
# itself be an empty list: pmap_has is the only call that actually
# distinguishes "absent" from "present but happens to look like the
# sentinel" -- never infer presence from pmap_get's return value alone.
# =============================================================================

make a function called pmap_new returns m
  return []
end

make a function called pmap_has takes m, key returns found
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] == key then
      return true
    end
    let i = i + 1
  end
  return false
end

# See the module-level warning above: [] means "not found" here, which is
# indistinguishable from a genuinely stored empty-list value. Call
# pmap_has first whenever that distinction matters.
make a function called pmap_get takes m, key returns value
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] == key then
      return m[i][1]
    end
    let i = i + 1
  end
  return []
end

make a function called pmap_put takes m, key, value returns m2
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] == key then
      return list_set(m, i, [key, value])
    end
    let i = i + 1
  end
  return list_push(m, [key, value])
end

make a function called pmap_remove takes m, key returns m2
  let out = []
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] != key then
      let out = list_push(out, m[i])
    end
    let i = i + 1
  end
  return out
end

make a function called pmap_keys takes m returns keys
  let out = []
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    let out = list_push(out, m[i][0])
    let i = i + 1
  end
  return out
end

make a function called pmap_size takes m returns n
  return to_num(list_len(m))
end

# =============================================================================
# schema_bdd: attach a Z-notation-style schema (declared state + a general
# invariant, plus named operations each with a require/ensure precondition/
# postcondition) to a BDD feature, and check a concrete Given/When/Then
# scenario as a WITNESS of that schema -- catching a scenario whose own
# Given already violates an operation's precondition, before any of the
# scenario's own Then assertions even run.
#
# Design decisions, and why (see the implementation plan this file was
# built from for the full investigation):
#
# - A schema's invariant/require/ensure are ORDINARY, separately-compiled
#   PatLang functions returning bool, referenced by name string and called
#   via apply() -- never the literal `require`/`ensure` keywords. Those
#   keywords lower to contract_check (rust-runtime/src/ir/hosts.rs), which
#   is FATAL on violation (confirmed directly, and independently documented
#   in self_hosting/lib/primitive_registry.patlang's own header) -- unusable
#   for a check that must report a diagnosis and keep running, the same
#   reason primitive_registry.patlang's own try_ wrappers never use
#   require/ensure for their real failure path either.
#
# - apply() has no argument-spread form (confirmed in
#   rust-runtime/src/ir/interpreter.rs): a function written once, generic
#   over any schema's own number of state variables, cannot pass one
#   positional argument per variable. State and inputs are therefore always
#   bundled as a single list argument: invariant_fn(state_list),
#   require_fn(state_list, input_list), ensure_fn(before_list, after_list,
#   input_list).
#
# - Binding extends the existing set_var/get("__vars", ...) convention
#   every Gherkin step in this codebase already uses (there is no
#   parametrized step-matching mechanism anywhere to extend instead --
#   step() dispatch is exact-literal-text, zero-argument, confirmed across
#   every existing _bdd_demo.patlang file). A scenario's own Given/Then step
#   functions call schema_bind_state/schema_bind_input directly.
#
# HARD RULE: self_hosting/lib/test.patlang's run_feature never resets bound
# vars between scenarios (only t_skipping/t_pending_tags are per-scenario).
# Every scenario's Given/Then must explicitly rebind every declared state
# variable and input itself, every time -- including restating an unchanged
# variable in Then. Do not rely on a value surviving from a previous
# scenario, and do not assume an unmentioned variable defaults to its
# "before" value in Then -- an omitted rebind reads back as the not-yet-
# bound sentinel (see schema_state_values below), which will correctly
# fail the check rather than silently pass, but the failure will look like
# a real violation unless this rule is followed.
# =============================================================================


# Single, process-wide registry (like Step's own new("Step", text)
# convention -- schemas and operations are inherently global, not
# per-instance, so one lazily-created Dict is simpler than
# primitive_registry.patlang's counter-named multi-registry support, which
# this doesn't need).
make a function called schema_registry returns registry
  let existing = get("__vars", "schema_bdd_registry_obj")
  if existing then
    return existing
  end
  let registry = new("Dict", "schema_bdd_registry")
  set_var("schema_bdd_registry_obj", registry)
  return registry
end

# state_var_names: list of strings naming the schema's declared state.
# invariant_fn: name of a function taking ONE argument (the state values,
# in the same order as state_var_names) and returning bool.
make a function called schema_define takes name, state_var_names, invariant_fn returns done
  send(schema_registry(), "set", name + "__schema", [state_var_names, invariant_fn])
  return true
end

make a function called schema_lookup takes name returns entry
  return get(schema_registry(), name + "__schema")
end

# input_names: list of strings naming the operation's declared inputs.
# require_fn: name of a function taking (state_values, input_values),
# returning bool -- the operation's precondition.
# ensure_fn: name of a function taking (before_values, after_values,
# input_values), returning bool -- the operation's postcondition.
make a function called schema_operation takes schema_name, op_name, input_names, require_fn, ensure_fn returns done
  send(schema_registry(), "set", schema_name + "::" + op_name + "__op", [schema_name, input_names, require_fn, ensure_fn])
  return true
end

make a function called schema_lookup_operation takes schema_name, op_name returns entry
  return get(schema_registry(), schema_name + "::" + op_name + "__op")
end

# ---- binding: a scenario's own step functions call these ----

make a function called schema_bind_state takes schema, var_name, phase, value returns done
  set_var(schema + "__" + var_name + "__" + phase, value)
  return true
end

make a function called schema_bind_input takes schema, op, param_name, value returns done
  set_var(schema + "__" + op + "__in__" + param_name, value)
  return true
end

# Not-yet-bound sentinel: get("__vars", ...) on an unset key -- same
# absence convention already relied on throughout this codebase (e.g.
# gherkin_contracts.patlang's `already_bound` check). Never distinguishes
# "never bound" from "bound to this same falsy value"; low risk for the
# LibraryLoans-shaped schemas this was designed against (string/list-typed
# state), a documented hard limit for anything boolean- or zero-valued.
make a function called schema_state_values takes schema, state_var_names returns values
  let out = []
  let i = 0
  let n = to_num(list_len(state_var_names))
  while i < n do
    let out = list_push(out, get("__vars", schema + "__" + state_var_names[i] + "__before"))
    let i = i + 1
  end
  return out
end

make a function called schema_state_values_after takes schema, state_var_names returns values
  let out = []
  let i = 0
  let n = to_num(list_len(state_var_names))
  while i < n do
    let out = list_push(out, get("__vars", schema + "__" + state_var_names[i] + "__after"))
    let i = i + 1
  end
  return out
end

make a function called schema_input_values takes schema, op, input_names returns values
  let out = []
  let i = 0
  let n = to_num(list_len(input_names))
  while i < n do
    let out = list_push(out, get("__vars", schema + "__" + op + "__in__" + input_names[i]))
    let i = i + 1
  end
  return out
end

# ---- the witness check ----
#
# Four-stage check, each stage its own diagnosis tag, checked in the order
# a Z schema's own reasoning goes: is the state even valid to start from,
# does this operation's precondition actually hold for it, does the
# claimed resulting state stay valid, and does the operation's own
# postcondition connect before to after correctly. Returns [tag, payload],
# the same 2-element diagnosis shape as synth5_induce
# (self_hosting/lib/synthesis_lgg.patlang) -- deliberately, so
# schema_format_diagnosis below can mirror synth5_format_diagnosis's own
# real structure rather than inventing a new diagnosis style.
# The value-based core: takes state_before/inputs/state_after directly
# rather than reading them out of the __vars binding store. schema_check
# below is the BDD-scenario-shaped wrapper around this; this function is
# what any OTHER caller (a synthesis harness, a future GOAP or ILP hook --
# see the implementation plan's Phase 3) should call directly instead of
# faking a scenario's Given/When/Then bindings just to reach schema_check.
make a function called schema_check_values takes schema_name, op_name, state_before, inputs, state_after returns diagnosis
  let schema_entry = schema_lookup(schema_name)
  let invariant_fn = schema_entry[1]

  let op_entry = schema_lookup_operation(schema_name, op_name)
  let require_fn = op_entry[2]
  let ensure_fn = op_entry[3]

  if apply(invariant_fn, state_before) == false then
    return ["invariant_violated_before", [schema_name, state_before]]
  end

  if apply(require_fn, state_before, inputs) == false then
    return ["precondition_violated", [op_name, state_before, inputs]]
  end

  if apply(invariant_fn, state_after) == false then
    return ["invariant_violated_after", [schema_name, state_after]]
  end

  if apply(ensure_fn, state_before, state_after, inputs) == false then
    return ["postcondition_violated", [op_name, state_before, state_after, inputs]]
  end

  return ["ok", [op_name, state_before, state_after, inputs]]
end

make a function called schema_check takes schema_name, op_name returns diagnosis
  let schema_entry = schema_lookup(schema_name)
  let state_var_names = schema_entry[0]

  let op_entry = schema_lookup_operation(schema_name, op_name)
  let input_names = op_entry[1]

  let state_before = schema_state_values(schema_name, state_var_names)
  let inputs = schema_input_values(schema_name, op_name, input_names)
  let state_after = schema_state_values_after(schema_name, state_var_names)
  return schema_check_values(schema_name, op_name, state_before, inputs, state_after)
end

# Mirrors synth5_format_diagnosis's real structure (synthesis_lgg.patlang):
# switch on diagnosis[0], build a human-readable question per case. Returns
# a plain list of question strings (empty for "ok"), same shape as
# synth5_induce_and_ask's own return convention.
make a function called schema_format_diagnosis takes schema_name, op_name, diagnosis returns questions
  let tag = diagnosis[0]
  let payload = diagnosis[1]

  if tag == "invariant_violated_before" then
    return ["This scenario's Given already leaves " + schema_name + " in a state that violates its own invariant, before " + op_name + " is even checked. Is the Given wrong, or is the invariant too strict?"]
  end

  if tag == "precondition_violated" then
    return ["Scenario claims " + op_name + " can run from this Given, but " + op_name + "'s own precondition returned false for these inputs. Is the Given wrong, or is " + op_name + "'s precondition too strict -- or is this scenario meant to test a rejection path, which needs its own operation schema rather than " + op_name + "'s?"]
  end

  if tag == "invariant_violated_after" then
    return ["Applying " + op_name + " produces a state that violates " + schema_name + "'s invariant. Is the Then clause's claimed resulting state wrong, or does " + op_name + " need a stronger precondition to rule this case out?"]
  end

  if tag == "postcondition_violated" then
    return ["The before/after state this scenario claims for " + op_name + " does not satisfy its own postcondition. Is the Then clause's claimed resulting state wrong, or is " + op_name + "'s postcondition wrong?"]
  end

  return []
end

# ---- synthesis integration (implementation plan Phase 3) ----
#
# Opt-in registration linking a SYNTHESIZED function's name to a schema
# operation it's meant to satisfy, plus a "harness" function name that
# knows how to actually exercise it: harness_fn takes (func_name) and
# returns [state_before, inputs, state_after] by calling the synthesized
# function itself (via apply) on some concrete test input and observing
# what it does. This is necessarily domain-specific -- there is no way to
# derive it generically -- so it must be supplied by whoever registers the
# hook, not synthesized here.
#
# Deliberately separate from schema_operation itself: a schema operation
# describes the CONTRACT; a synthesis hook additionally says "and here's
# how to actually run a candidate implementation against it," which only
# matters once there's a synthesized candidate to check, not for the
# scenario-witnessing use in schema_check above.
make a function called schema_register_synthesis_check takes func_name, schema_name, op_name, harness_fn returns done
  send(schema_registry(), "set", func_name + "__synthesis_check", [schema_name, op_name, harness_fn])
  return true
end

make a function called schema_lookup_synthesis_check takes func_name returns entry
  return get(schema_registry(), func_name + "__synthesis_check")
end

# Runs a registered synthesis hook for func_name and returns its
# schema_check_values diagnosis directly. Callers with no hook registered
# for func_name should skip calling this entirely (schema_lookup_
# synthesis_check(func_name) is falsy) rather than call it and inspect the
# result -- there is no "no hook registered" diagnosis tag, since this
# function assumes a hook exists.
make a function called schema_run_synthesis_check takes func_name returns diagnosis
  let hook = schema_lookup_synthesis_check(func_name)
  let schema_name = hook[0]
  let op_name = hook[1]
  let harness_fn = hook[2]
  let triple = apply(harness_fn, func_name)
  return schema_check_values(schema_name, op_name, triple[0], triple[1], triple[2])
end
# Selftest for self_hosting/lib/schema_bdd.patlang: the LibraryLoans/
# BorrowBook worked example from the teaching site's "Schemas and
# Scenarios" page and the implementation plan built from it. Proven through
# the real Gherkin runner (run_feature), not by calling schema_check
# directly -- the point is proving the BDD-integration path works, not
# just the underlying function.
#
# Run from the repo root:
#   rust-runtime/target/release/pat --ir-run self_hosting/schema_bdd_selftest.patlang


# ---- LibraryLoans schema: invariant + BorrowBook's precondition/postcondition ----
#
# state = [books, borrowedBy]. Invariant: every title on loan is a title
# the library actually holds -- dom borrowedBy subset_of books, in the
# teaching page's own Z notation.
make a function called schema_inv_library_loans takes state returns ok
  let books = state[0]
  let borrowedBy = state[1]
  let keys = pmap_keys(borrowedBy)
  let i = 0
  let n = to_num(list_len(keys))
  while i < n do
    if pset_contains(books, keys[i]) == false then
      return false
    end
    let i = i + 1
  end
  return true
end

# BorrowBook's precondition: the title exists and isn't already on loan.
make a function called schema_require_borrow_book takes state, inputs returns ok
  let books = state[0]
  let borrowedBy = state[1]
  let title = inputs[0]
  if pset_contains(books, title) == false then
    return false
  end
  return pmap_has(borrowedBy, title) == false
end

# BorrowBook's postcondition: the set of titles is unchanged (borrowing
# doesn't add or remove books), and borrowedBy after equals borrowedBy
# before with exactly [title -> member] added.
make a function called schema_ensure_borrow_book takes before, after, inputs returns ok
  let books_before = before[0]
  let borrowedBy_before = before[1]
  let books_after = after[0]
  let borrowedBy_after = after[1]
  let title = inputs[0]
  let member = inputs[1]
  if pset_equal(books_before, books_after) == false then
    return false
  end
  let expected_after = pmap_put(borrowedBy_before, title, member)
  return schema_pmap_equal(expected_after, borrowedBy_after)
end

# pmap.patlang has no pmap_equal (not needed by pset/pmap's own selftests);
# small enough to define locally here rather than grow pmap.patlang's
# surface for a single caller.
make a function called schema_pmap_equal takes a, b returns eq
  if pmap_size(a) != pmap_size(b) then
    return false
  end
  let keys = pmap_keys(a)
  let i = 0
  let n = to_num(list_len(keys))
  while i < n do
    let k = keys[i]
    if pmap_has(b, k) == false then
      return false
    end
    if pmap_get(a, k) != pmap_get(b, k) then
      return false
    end
    let i = i + 1
  end
  return true
end

make a function called register_library_loans_schema returns done
  schema_define("LibraryLoans", ["books", "borrowedBy"], "schema_inv_library_loans")
  schema_operation("LibraryLoans", "BorrowBook", ["title", "member"], "schema_require_borrow_book", "schema_ensure_borrow_book")
  return true
end

# ---- step definitions ----

make a function called st_given_library_holds_dune returns done
  schema_bind_state("LibraryLoans", "books", "before", pset_add(pset_new(), "Dune"))
  return true
end

make a function called st_given_dune_not_borrowed returns done
  schema_bind_state("LibraryLoans", "borrowedBy", "before", pmap_new())
  return true
end

make a function called st_given_dune_borrowed_by_okonkwo returns done
  schema_bind_state("LibraryLoans", "borrowedBy", "before", pmap_put(pmap_new(), "Dune", "S. Okonkwo"))
  return true
end

make a function called st_when_diallo_borrows_dune returns done
  schema_bind_input("LibraryLoans", "BorrowBook", "title", "Dune")
  schema_bind_input("LibraryLoans", "BorrowBook", "member", "A. Diallo")
  return true
end

# The scenario's own claimed outcome: books unchanged, Dune now on loan to
# Diallo. Restates books explicitly per schema_bdd.patlang's hard rule
# (every scenario must rebind every declared state var in Then, never rely
# on a default).
make a function called st_then_dune_borrowed_by_diallo returns done
  let before_books = get("__vars", "LibraryLoans__books__before")
  schema_bind_state("LibraryLoans", "books", "after", before_books)
  let before_borrowedBy = get("__vars", "LibraryLoans__borrowedBy__before")
  schema_bind_state("LibraryLoans", "borrowedBy", "after", pmap_put(before_borrowedBy, "Dune", "A. Diallo"))
  let diagnosis = schema_check("LibraryLoans", "BorrowBook")
  check("borrowing an available title is accepted by the schema", diagnosis[0], "ok")
  return true
end

# Deliberately does NOT bind an "after" state -- schema_check's own
# ordering (invariant -> precondition -> invariant-after -> postcondition)
# means a precondition failure is reported before "after" is ever read, so
# there is nothing to claim here: the request never gets that far.
make a function called st_then_system_rejects_request returns done
  let diagnosis = schema_check("LibraryLoans", "BorrowBook")
  check("borrowing an already-borrowed title is rejected by the schema", diagnosis[0], "precondition_violated")
  let questions = schema_format_diagnosis("LibraryLoans", "BorrowBook", diagnosis)
  check("a rejected scenario gets exactly one diagnostic question", to_num(list_len(questions)), 1)
  check("the diagnostic question is non-empty", questions[0].length > 0, true)
  return true
end

make a function called register_library_loans_steps returns done
  step("the library holds \"Dune\"", "st_given_library_holds_dune")
  step("\"Dune\" is not currently borrowed", "st_given_dune_not_borrowed")
  step("\"Dune\" is currently borrowed by \"S. Okonkwo\"", "st_given_dune_borrowed_by_okonkwo")
  step("\"A. Diallo\" borrows \"Dune\"", "st_when_diallo_borrows_dune")
  step("\"Dune\" is borrowed by \"A. Diallo\"", "st_then_dune_borrowed_by_diallo")
  step("the system rejects the request", "st_then_system_rejects_request")
  return true
end

make a function called library_loans_feature returns text
  return "Feature: Library loans

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\"

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
"
end

make a function called run_schema_bdd_selftest returns ok
  t_init()
  register_library_loans_schema()
  register_library_loans_steps()
  run_feature(library_loans_feature())
  t_report()
  return get("__vars", "t_fail") == 0
end

run_schema_bdd_selftest()

# =============================================================================
# Test framework (Stage 1 dialect): unit assertions plus a Gherkin-style
# feature runner. Step definitions are registered in the object store keyed
# by their text; features are plain text dispatched line by line, so the
# same framework covers unit, integration, and behaviour tests.
# =============================================================================

make a function called t_init returns done
  set_var("t_pass", 0)
  set_var("t_fail", 0)
  set_var("t_tagfilter", "")
  set_var("t_pending_tags", "")
  set_var("t_skipping", 0)
  return true
end

make a function called contains_text takes hay, needle returns r
  if needle.length > hay.length then
    return false
  end
  let i = 0
  while i <= hay.length - needle.length do
    if substr(hay, i, needle.length) == needle then
      return true
    end
    let i = i + 1
  end
  return false
end

make a function called check takes label, actual, expected returns ok
  if actual == expected then
    set_var("t_pass", get("__vars", "t_pass") + 1)
    print("  ok: " + label)
    return true
  else
    set_var("t_fail", get("__vars", "t_fail") + 1)
    print("  FAIL: " + label + " (got " + actual + ", want " + expected + ")")
    return false
  end
end

make a function called t_report returns ok
  let p = get("__vars", "t_pass")
  let f = get("__vars", "t_fail")
  print("tests: " + p + " passed, " + f + " failed")
  if f == 0 then
    print("ALL TESTS PASSED")
    return true
  else
    print("TESTS FAILED")
    return false
  end
end

# ---- Gherkin runner ----

# Register a step: step("a fresh till", "st_fresh_till")
make a function called step takes text, fname returns done
  new("Step", text)
  send(text, "set", "fn", fname)
  return true
end

make a function called starts_with takes s, prefix returns r
  if s.length < prefix.length then
    return false
  end
  return substr(s, 0, prefix.length) == prefix
end

make a function called trim_left takes s returns out
  let i = 0
  let scanning = true
  while (i < s.length) and scanning do
    let c = char_code(s, i)
    if (c == 32) or (c == 9) then
      let i = i + 1
    else
      let scanning = false
    end
  end
  return substr(s, i, s.length - i)
end

# Strip a Gherkin keyword; returns the step text or "" if not a step line
make a function called step_text takes line returns out
  if starts_with(line, "Given ") then
    return substr(line, 6, line.length - 6)
  end
  if starts_with(line, "When ") then
    return substr(line, 5, line.length - 5)
  end
  if starts_with(line, "Then ") then
    return substr(line, 5, line.length - 5)
  end
  if starts_with(line, "And ") then
    return substr(line, 4, line.length - 4)
  end
  return ""
end

# Run only scenarios whose preceding @tag line contains `tag` ("" = all)
make a function called run_feature_tagged takes feature, tag returns ok
  set_var("t_tagfilter", tag)
  return run_feature(feature)
end

make a function called run_feature_file takes path returns ok
  return run_feature(read_file(path))
end

make a function called run_feature takes feature returns ok
  let h = str_intern(feature)
  let n = sc_len(h)
  let i = 0
  let line = sb_new()
  while i <= n do
    let c = sc_code(h, i)
    if (c == 10) or (c == -1) then
      let raw = trim_left(sb_str(line))
      let line = sb_new()
      if starts_with(raw, "@") then
        set_var("t_pending_tags", raw)
      end
      if starts_with(raw, "Feature:") then
        print(raw)
      end
      if starts_with(raw, "Scenario:") then
        let filter = get("__vars", "t_tagfilter")
        let tags = get("__vars", "t_pending_tags")
        set_var("t_pending_tags", "")
        if filter then
          if tags then
            if contains_text(tags, filter) then
              set_var("t_skipping", 0)
              print(raw + "  [" + tags + "]")
            else
              set_var("t_skipping", 1)
              print(raw + "  [skipped: needs " + filter + "]")
            end
          else
            set_var("t_skipping", 1)
            print(raw + "  [skipped: needs " + filter + "]")
          end
        else
          set_var("t_skipping", 0)
          print(raw)
        end
      else
        let text = step_text(raw)
        if (text != "") and (get("__vars", "t_skipping") != 1) then
          if starts_with(text, "require ") then
            handle_contract_step("require", substr(text, 8, text.length - 8))
          else
            if starts_with(text, "ensure ") then
              handle_contract_step("ensure", substr(text, 7, text.length - 7))
            else
              let fname = get(text, "fn")
              if fname then
                apply(fname)
              else
                set_var("t_fail", get("__vars", "t_fail") + 1)
                print("  FAIL: undefined step: " + text)
              end
            end
          end
        end
      end
      let i = i + 1
    else
      if c == 13 then
        let i = i + 1
      else
        sb_push(line, sc_char(h, i))
        let i = i + 1
      end
    end
  end
  return true
end

# =============================================================================
# pset: a minimal Set<T> built on a plain list with linear-scan membership,
# the same idiom already used by depgraph_list_contains and
# synth5_list_contains (self_hosting/lib/depgraph.patlang,
# self_hosting/lib/synthesis_lgg.patlang) rather than a new primitive --
# PatLang has no native Set type.
#
# Functional / return-new-collection style throughout (mirrors list_push's
# own semantics): every mutating-sounding operation returns a NEW list
# rather than mutating in place. This matters specifically for schema_bdd's
# before/after snapshotting, which needs an independent copy of state at
# two points in time -- an in-place structure would make "before" silently
# turn into "after" once the operation runs.
# =============================================================================

make a function called pset_new returns s
  return []
end

make a function called pset_contains takes s, item returns found
  let i = 0
  let n = to_num(list_len(s))
  while i < n do
    if s[i] == item then
      return true
    end
    let i = i + 1
  end
  return false
end

make a function called pset_add takes s, item returns s2
  if pset_contains(s, item) then
    return s
  end
  return list_push(s, item)
end

make a function called pset_remove takes s, item returns s2
  let out = []
  let i = 0
  let n = to_num(list_len(s))
  while i < n do
    if s[i] != item then
      let out = list_push(out, s[i])
    end
    let i = i + 1
  end
  return out
end

make a function called pset_size takes s returns n
  return to_num(list_len(s))
end

# Identity -- exposed so callers iterating a set's members don't need to
# know it's "just a list" internally; the name documents intent at the
# call site instead.
make a function called pset_to_list takes s returns items
  return s
end

# Set equality: same size, and every member of a is in b. Given pset_add's
# own dedup, equal size plus one-directional containment implies the
# reverse containment too (no way for b to hold something a doesn't
# without differing in size).
make a function called pset_equal takes a, b returns eq
  if pset_size(a) != pset_size(b) then
    return false
  end
  let i = 0
  let n = to_num(list_len(a))
  while i < n do
    if pset_contains(b, a[i]) == false then
      return false
    end
    let i = i + 1
  end
  return true
end

# =============================================================================
# pmap: a minimal Map<K,V> as an association list of [key, value] pairs with
# linear-scan lookup -- the exact same idiom already proven in
# self_hosting/lib/depgraph.patlang's depgraph_map_get/depgraph_map_append
# (a file->list-of-files map), generalised here to an arbitrary value type
# and given a full put/get/has/remove/keys surface. PatLang has no native
# Map/Dict type usable from self-hosted code at this scale.
#
# Functional / return-new-collection style throughout, for the same reason
# as pset.patlang: schema_bdd needs an independent before/after snapshot of
# state, which an in-place-mutating map wouldn't give for free.
#
# pmap_get returns [] (an empty list) for a missing key -- the same
# not-found sentinel depgraph_map_get already uses, not a distinct "Unit"
# literal (PatLang's dialect has no source-level Unit/nil literal to write
# directly). This is INHERENTLY AMBIGUOUS if a real stored value could
# itself be an empty list: pmap_has is the only call that actually
# distinguishes "absent" from "present but happens to look like the
# sentinel" -- never infer presence from pmap_get's return value alone.
# =============================================================================

make a function called pmap_new returns m
  return []
end

make a function called pmap_has takes m, key returns found
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] == key then
      return true
    end
    let i = i + 1
  end
  return false
end

# See the module-level warning above: [] means "not found" here, which is
# indistinguishable from a genuinely stored empty-list value. Call
# pmap_has first whenever that distinction matters.
make a function called pmap_get takes m, key returns value
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] == key then
      return m[i][1]
    end
    let i = i + 1
  end
  return []
end

make a function called pmap_put takes m, key, value returns m2
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] == key then
      return list_set(m, i, [key, value])
    end
    let i = i + 1
  end
  return list_push(m, [key, value])
end

make a function called pmap_remove takes m, key returns m2
  let out = []
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    if m[i][0] != key then
      let out = list_push(out, m[i])
    end
    let i = i + 1
  end
  return out
end

make a function called pmap_keys takes m returns keys
  let out = []
  let i = 0
  let n = to_num(list_len(m))
  while i < n do
    let out = list_push(out, m[i][0])
    let i = i + 1
  end
  return out
end

make a function called pmap_size takes m returns n
  return to_num(list_len(m))
end

# =============================================================================
# schema_bdd: attach a Z-notation-style schema (declared state + a general
# invariant, plus named operations each with a require/ensure precondition/
# postcondition) to a BDD feature, and check a concrete Given/When/Then
# scenario as a WITNESS of that schema -- catching a scenario whose own
# Given already violates an operation's precondition, before any of the
# scenario's own Then assertions even run.
#
# Design decisions, and why (see the implementation plan this file was
# built from for the full investigation):
#
# - A schema's invariant/require/ensure are ORDINARY, separately-compiled
#   PatLang functions returning bool, referenced by name string and called
#   via apply() -- never the literal `require`/`ensure` keywords. Those
#   keywords lower to contract_check (rust-runtime/src/ir/hosts.rs), which
#   is FATAL on violation (confirmed directly, and independently documented
#   in self_hosting/lib/primitive_registry.patlang's own header) -- unusable
#   for a check that must report a diagnosis and keep running, the same
#   reason primitive_registry.patlang's own try_ wrappers never use
#   require/ensure for their real failure path either.
#
# - apply() has no argument-spread form (confirmed in
#   rust-runtime/src/ir/interpreter.rs): a function written once, generic
#   over any schema's own number of state variables, cannot pass one
#   positional argument per variable. State and inputs are therefore always
#   bundled as a single list argument: invariant_fn(state_list),
#   require_fn(state_list, input_list), ensure_fn(before_list, after_list,
#   input_list).
#
# - Binding extends the existing set_var/get("__vars", ...) convention
#   every Gherkin step in this codebase already uses (there is no
#   parametrized step-matching mechanism anywhere to extend instead --
#   step() dispatch is exact-literal-text, zero-argument, confirmed across
#   every existing _bdd_demo.patlang file). A scenario's own Given/Then step
#   functions call schema_bind_state/schema_bind_input directly.
#
# HARD RULE: self_hosting/lib/test.patlang's run_feature never resets bound
# vars between scenarios (only t_skipping/t_pending_tags are per-scenario).
# Every scenario's Given/Then must explicitly rebind every declared state
# variable and input itself, every time -- including restating an unchanged
# variable in Then. Do not rely on a value surviving from a previous
# scenario, and do not assume an unmentioned variable defaults to its
# "before" value in Then -- an omitted rebind reads back as the not-yet-
# bound sentinel (see schema_state_values below), which will correctly
# fail the check rather than silently pass, but the failure will look like
# a real violation unless this rule is followed.
# =============================================================================


# Single, process-wide registry (like Step's own new("Step", text)
# convention -- schemas and operations are inherently global, not
# per-instance, so one lazily-created Dict is simpler than
# primitive_registry.patlang's counter-named multi-registry support, which
# this doesn't need).
make a function called schema_registry returns registry
  let existing = get("__vars", "schema_bdd_registry_obj")
  if existing then
    return existing
  end
  let registry = new("Dict", "schema_bdd_registry")
  set_var("schema_bdd_registry_obj", registry)
  return registry
end

# state_var_names: list of strings naming the schema's declared state.
# invariant_fn: name of a function taking ONE argument (the state values,
# in the same order as state_var_names) and returning bool.
make a function called schema_define takes name, state_var_names, invariant_fn returns done
  send(schema_registry(), "set", name + "__schema", [state_var_names, invariant_fn])
  return true
end

make a function called schema_lookup takes name returns entry
  return get(schema_registry(), name + "__schema")
end

# input_names: list of strings naming the operation's declared inputs.
# require_fn: name of a function taking (state_values, input_values),
# returning bool -- the operation's precondition.
# ensure_fn: name of a function taking (before_values, after_values,
# input_values), returning bool -- the operation's postcondition.
make a function called schema_operation takes schema_name, op_name, input_names, require_fn, ensure_fn returns done
  send(schema_registry(), "set", schema_name + "::" + op_name + "__op", [schema_name, input_names, require_fn, ensure_fn])
  return true
end

make a function called schema_lookup_operation takes schema_name, op_name returns entry
  return get(schema_registry(), schema_name + "::" + op_name + "__op")
end

# ---- binding: a scenario's own step functions call these ----

make a function called schema_bind_state takes schema, var_name, phase, value returns done
  set_var(schema + "__" + var_name + "__" + phase, value)
  return true
end

make a function called schema_bind_input takes schema, op, param_name, value returns done
  set_var(schema + "__" + op + "__in__" + param_name, value)
  return true
end

# Not-yet-bound sentinel: get("__vars", ...) on an unset key -- same
# absence convention already relied on throughout this codebase (e.g.
# gherkin_contracts.patlang's `already_bound` check). Never distinguishes
# "never bound" from "bound to this same falsy value"; low risk for the
# LibraryLoans-shaped schemas this was designed against (string/list-typed
# state), a documented hard limit for anything boolean- or zero-valued.
make a function called schema_state_values takes schema, state_var_names returns values
  let out = []
  let i = 0
  let n = to_num(list_len(state_var_names))
  while i < n do
    let out = list_push(out, get("__vars", schema + "__" + state_var_names[i] + "__before"))
    let i = i + 1
  end
  return out
end

make a function called schema_state_values_after takes schema, state_var_names returns values
  let out = []
  let i = 0
  let n = to_num(list_len(state_var_names))
  while i < n do
    let out = list_push(out, get("__vars", schema + "__" + state_var_names[i] + "__after"))
    let i = i + 1
  end
  return out
end

make a function called schema_input_values takes schema, op, input_names returns values
  let out = []
  let i = 0
  let n = to_num(list_len(input_names))
  while i < n do
    let out = list_push(out, get("__vars", schema + "__" + op + "__in__" + input_names[i]))
    let i = i + 1
  end
  return out
end

# ---- the witness check ----
#
# Four-stage check, each stage its own diagnosis tag, checked in the order
# a Z schema's own reasoning goes: is the state even valid to start from,
# does this operation's precondition actually hold for it, does the
# claimed resulting state stay valid, and does the operation's own
# postcondition connect before to after correctly. Returns [tag, payload],
# the same 2-element diagnosis shape as synth5_induce
# (self_hosting/lib/synthesis_lgg.patlang) -- deliberately, so
# schema_format_diagnosis below can mirror synth5_format_diagnosis's own
# real structure rather than inventing a new diagnosis style.
# The value-based core: takes state_before/inputs/state_after directly
# rather than reading them out of the __vars binding store. schema_check
# below is the BDD-scenario-shaped wrapper around this; this function is
# what any OTHER caller (a synthesis harness, a future GOAP or ILP hook --
# see the implementation plan's Phase 3) should call directly instead of
# faking a scenario's Given/When/Then bindings just to reach schema_check.
make a function called schema_check_values takes schema_name, op_name, state_before, inputs, state_after returns diagnosis
  let schema_entry = schema_lookup(schema_name)
  let invariant_fn = schema_entry[1]

  let op_entry = schema_lookup_operation(schema_name, op_name)
  let require_fn = op_entry[2]
  let ensure_fn = op_entry[3]

  if apply(invariant_fn, state_before) == false then
    return ["invariant_violated_before", [schema_name, state_before]]
  end

  if apply(require_fn, state_before, inputs) == false then
    return ["precondition_violated", [op_name, state_before, inputs]]
  end

  if apply(invariant_fn, state_after) == false then
    return ["invariant_violated_after", [schema_name, state_after]]
  end

  if apply(ensure_fn, state_before, state_after, inputs) == false then
    return ["postcondition_violated", [op_name, state_before, state_after, inputs]]
  end

  return ["ok", [op_name, state_before, state_after, inputs]]
end

make a function called schema_check takes schema_name, op_name returns diagnosis
  let schema_entry = schema_lookup(schema_name)
  let state_var_names = schema_entry[0]

  let op_entry = schema_lookup_operation(schema_name, op_name)
  let input_names = op_entry[1]

  let state_before = schema_state_values(schema_name, state_var_names)
  let inputs = schema_input_values(schema_name, op_name, input_names)
  let state_after = schema_state_values_after(schema_name, state_var_names)
  return schema_check_values(schema_name, op_name, state_before, inputs, state_after)
end

# Mirrors synth5_format_diagnosis's real structure (synthesis_lgg.patlang):
# switch on diagnosis[0], build a human-readable question per case. Returns
# a plain list of question strings (empty for "ok"), same shape as
# synth5_induce_and_ask's own return convention.
make a function called schema_format_diagnosis takes schema_name, op_name, diagnosis returns questions
  let tag = diagnosis[0]
  let payload = diagnosis[1]

  if tag == "invariant_violated_before" then
    return ["This scenario's Given already leaves " + schema_name + " in a state that violates its own invariant, before " + op_name + " is even checked. Is the Given wrong, or is the invariant too strict?"]
  end

  if tag == "precondition_violated" then
    return ["Scenario claims " + op_name + " can run from this Given, but " + op_name + "'s own precondition returned false for these inputs. Is the Given wrong, or is " + op_name + "'s precondition too strict -- or is this scenario meant to test a rejection path, which needs its own operation schema rather than " + op_name + "'s?"]
  end

  if tag == "invariant_violated_after" then
    return ["Applying " + op_name + " produces a state that violates " + schema_name + "'s invariant. Is the Then clause's claimed resulting state wrong, or does " + op_name + " need a stronger precondition to rule this case out?"]
  end

  if tag == "postcondition_violated" then
    return ["The before/after state this scenario claims for " + op_name + " does not satisfy its own postcondition. Is the Then clause's claimed resulting state wrong, or is " + op_name + "'s postcondition wrong?"]
  end

  return []
end

# ---- synthesis integration (implementation plan Phase 3) ----
#
# Opt-in registration linking a SYNTHESIZED function's name to a schema
# operation it's meant to satisfy, plus a "harness" function name that
# knows how to actually exercise it: harness_fn takes (func_name) and
# returns [state_before, inputs, state_after] by calling the synthesized
# function itself (via apply) on some concrete test input and observing
# what it does. This is necessarily domain-specific -- there is no way to
# derive it generically -- so it must be supplied by whoever registers the
# hook, not synthesized here.
#
# Deliberately separate from schema_operation itself: a schema operation
# describes the CONTRACT; a synthesis hook additionally says "and here's
# how to actually run a candidate implementation against it," which only
# matters once there's a synthesized candidate to check, not for the
# scenario-witnessing use in schema_check above.
make a function called schema_register_synthesis_check takes func_name, schema_name, op_name, harness_fn returns done
  send(schema_registry(), "set", func_name + "__synthesis_check", [schema_name, op_name, harness_fn])
  return true
end

make a function called schema_lookup_synthesis_check takes func_name returns entry
  return get(schema_registry(), func_name + "__synthesis_check")
end

# Runs a registered synthesis hook for func_name and returns its
# schema_check_values diagnosis directly. Callers with no hook registered
# for func_name should skip calling this entirely (schema_lookup_
# synthesis_check(func_name) is falsy) rather than call it and inspect the
# result -- there is no "no hook registered" diagnosis tag, since this
# function assumes a hook exists.
make a function called schema_run_synthesis_check takes func_name returns diagnosis
  let hook = schema_lookup_synthesis_check(func_name)
  let schema_name = hook[0]
  let op_name = hook[1]
  let harness_fn = hook[2]
  let triple = apply(harness_fn, func_name)
  return schema_check_values(schema_name, op_name, triple[0], triple[1], triple[2])
end
# =============================================================================
# LibraryLoans, fully worked: a richer Z/BDD hybrid schema than the plan's
# own minimal selftest (self_hosting/schema_bdd_selftest.patlang) --
# three pieces of interacting state, a multi-clause precondition, a
# cross-cutting invariant (no member may exceed three simultaneous
# loans), and enough scenarios to exercise every diagnosis tag
# schema_check can produce: invariant_violated_before, precondition_
# violated, postcondition_violated, and ok. Companion to the parslow.net
# "Schemas and Scenarios" page.
#
# State: books (Set<Title>), borrowedBy (Map<Title,Member>), loanCount
# (Map<Member,Int>) -- loanCount is tracked SEPARATELY from borrowedBy
# rather than recomputed from it on every check, the same design choice
# a real system would make (a denormalised, maintained count rather than
# a full table scan every time), which is exactly why BorrowBook/
# ReturnBook's own postconditions -- not just the invariant -- have real
# work to do keeping the two consistent with each other.
#
# Run from the repo root:
#   rust-runtime/target/release/pat --ir-run self_hosting/examples/library_loans_schema_demo.patlang


# ---- LibraryLoans: invariant + BorrowBook/ReturnBook contracts ----

make a function called ll_loan_count_of takes loan_count, member returns n
  if pmap_has(loan_count, member) then
    return pmap_get(loan_count, member)
  end
  return 0
end

# Invariant: every title on loan is one the library actually holds, and
# no member exceeds three simultaneous loans -- the second half is a
# genuine cross-cutting business rule, not derivable from the first.
make a function called ll_invariant takes state returns ok
  let books = state[0]
  let borrowed_by = state[1]
  let loan_count = state[2]
  let keys = pmap_keys(borrowed_by)
  let i = 0
  let n = to_num(list_len(keys))
  while i < n do
    if pset_contains(books, keys[i]) == false then
      return false
    end
    let i = i + 1
  end
  let members = pmap_keys(loan_count)
  let j = 0
  let mn = to_num(list_len(members))
  while j < mn do
    let count = pmap_get(loan_count, members[j])
    if (count < 0) or (count > 3) then
      return false
    end
    let j = j + 1
  end
  return true
end

# BorrowBook's precondition is three independent clauses, checked
# together -- exactly the shape a hand-written scenario can violate in
# three genuinely different ways, each needing its own scenario to
# demonstrate (see the feature text below).
make a function called ll_require_borrow takes state, inputs returns ok
  let books = state[0]
  let borrowed_by = state[1]
  let loan_count = state[2]
  let title = inputs[0]
  let member = inputs[1]
  if pset_contains(books, title) == false then
    return false
  end
  if pmap_has(borrowed_by, title) then
    return false
  end
  return ll_loan_count_of(loan_count, member) < 3
end

make a function called ll_ensure_borrow takes before, after, inputs returns ok
  let books_before = before[0]
  let borrowed_by_before = before[1]
  let loan_count_before = before[2]
  let books_after = after[0]
  let borrowed_by_after = after[1]
  let loan_count_after = after[2]
  let title = inputs[0]
  let member = inputs[1]
  if pset_equal(books_before, books_after) == false then
    return false
  end
  let expected_borrowed_by = pmap_put(borrowed_by_before, title, member)
  if schema_pmap_equal(expected_borrowed_by, borrowed_by_after) == false then
    return false
  end
  let expected_count = ll_loan_count_of(loan_count_before, member) + 1
  let expected_loan_count = pmap_put(loan_count_before, member, expected_count)
  return schema_pmap_equal(expected_loan_count, loan_count_after)
end

# ReturnBook takes only the title -- the member is recovered from
# borrowedBy, exactly the way a real return desk works (you hand back
# the book, not a signed claim of who you are).
make a function called ll_require_return takes state, inputs returns ok
  let borrowed_by = state[1]
  let title = inputs[0]
  return pmap_has(borrowed_by, title)
end

make a function called ll_ensure_return takes before, after, inputs returns ok
  let books_before = before[0]
  let borrowed_by_before = before[1]
  let loan_count_before = before[2]
  let books_after = after[0]
  let borrowed_by_after = after[1]
  let loan_count_after = after[2]
  let title = inputs[0]
  let member = pmap_get(borrowed_by_before, title)
  if pset_equal(books_before, books_after) == false then
    return false
  end
  let expected_borrowed_by = pmap_remove(borrowed_by_before, title)
  if schema_pmap_equal(expected_borrowed_by, borrowed_by_after) == false then
    return false
  end
  let expected_count = ll_loan_count_of(loan_count_before, member) - 1
  let expected_loan_count = pmap_put(loan_count_before, member, expected_count)
  return schema_pmap_equal(expected_loan_count, loan_count_after)
end

# pmap.patlang has no pmap_equal (see schema_bdd_selftest.patlang's own
# note on this); defined once here, shared by both ensure functions.
make a function called schema_pmap_equal takes a, b returns eq
  if pmap_size(a) != pmap_size(b) then
    return false
  end
  let keys = pmap_keys(a)
  let i = 0
  let n = to_num(list_len(keys))
  while i < n do
    let k = keys[i]
    if pmap_has(b, k) == false then
      return false
    end
    if pmap_get(a, k) != pmap_get(b, k) then
      return false
    end
    let i = i + 1
  end
  return true
end

make a function called register_library_loans_schema returns done
  schema_define("LibraryLoans", ["books", "borrowedBy", "loanCount"], "ll_invariant")
  schema_operation("LibraryLoans", "BorrowBook", ["title", "member"], "ll_require_borrow", "ll_ensure_borrow")
  schema_operation("LibraryLoans", "ReturnBook", ["title"], "ll_require_return", "ll_ensure_return")
  return true
end

# ---- step definitions ----

make a function called ll_standard_catalogue returns s
  let s = pset_add(pset_new(), "Dune")
  let s = pset_add(s, "Neuromancer")
  let s = pset_add(s, "Foundation")
  return s
end

make a function called st_given_standard_catalogue returns done
  schema_bind_state("LibraryLoans", "books", "before", ll_standard_catalogue())
  return true
end

make a function called st_given_no_loans_out returns done
  schema_bind_state("LibraryLoans", "borrowedBy", "before", pmap_new())
  schema_bind_state("LibraryLoans", "loanCount", "before", pmap_new())
  return true
end

make a function called st_given_dune_borrowed_by_okonkwo returns done
  schema_bind_state("LibraryLoans", "borrowedBy", "before", pmap_put(pmap_new(), "Dune", "S. Okonkwo"))
  schema_bind_state("LibraryLoans", "loanCount", "before", pmap_put(pmap_new(), "S. Okonkwo", 1))
  return true
end

# Deliberately consistent, valid "already at the limit" state -- three
# real titles, all correctly attributed to the same member, matching
# what the invariant actually checks (the count, not the specific books).
make a function called st_given_diallo_at_loan_limit returns done
  let borrowed_by = pmap_put(pmap_new(), "Dune", "A. Diallo")
  let borrowed_by = pmap_put(borrowed_by, "Neuromancer", "A. Diallo")
  let borrowed_by = pmap_put(borrowed_by, "Foundation", "A. Diallo")
  schema_bind_state("LibraryLoans", "borrowedBy", "before", borrowed_by)
  schema_bind_state("LibraryLoans", "loanCount", "before", pmap_put(pmap_new(), "A. Diallo", 3))
  return true
end

# Deliberately INVALID state: the record already claims four loans,
# violating the invariant before any operation is even attempted.
make a function called st_given_corrupted_loan_record returns done
  schema_bind_state("LibraryLoans", "borrowedBy", "before", pmap_new())
  schema_bind_state("LibraryLoans", "loanCount", "before", pmap_put(pmap_new(), "A. Diallo", 4))
  return true
end

make a function called st_when_diallo_borrows_foundation returns done
  schema_bind_input("LibraryLoans", "BorrowBook", "title", "Foundation")
  schema_bind_input("LibraryLoans", "BorrowBook", "member", "A. Diallo")
  return true
end

make a function called st_when_diallo_borrows_dune returns done
  schema_bind_input("LibraryLoans", "BorrowBook", "title", "Dune")
  schema_bind_input("LibraryLoans", "BorrowBook", "member", "A. Diallo")
  return true
end

make a function called st_when_okonkwo_returns_dune returns done
  schema_bind_input("LibraryLoans", "ReturnBook", "title", "Dune")
  return true
end

make a function called st_when_someone_returns_foundation returns done
  schema_bind_input("LibraryLoans", "ReturnBook", "title", "Foundation")
  return true
end

# ---- Then steps: state the scenario's own claim, then check it ----

make a function called ll_check takes op, expected_tag, label returns done
  let diagnosis = schema_check("LibraryLoans", op)
  check(label, diagnosis[0], expected_tag)
  return true
end

make a function called st_then_foundation_correctly_recorded returns done
  let before_books = get("__vars", "LibraryLoans__books__before")
  schema_bind_state("LibraryLoans", "books", "after", before_books)
  let before_borrowed_by = get("__vars", "LibraryLoans__borrowedBy__before")
  schema_bind_state("LibraryLoans", "borrowedBy", "after", pmap_put(before_borrowed_by, "Foundation", "A. Diallo"))
  let before_loan_count = get("__vars", "LibraryLoans__loanCount__before")
  schema_bind_state("LibraryLoans", "loanCount", "after", pmap_put(before_loan_count, "A. Diallo", ll_loan_count_of(before_loan_count, "A. Diallo") + 1))
  ll_check("BorrowBook", "ok", "borrowing an available title, under the loan limit, is accepted")
  return true
end

make a function called st_then_borrow_rejected_already_out returns done
  ll_check("BorrowBook", "precondition_violated", "borrowing a title someone else already has out is rejected")
  return true
end

make a function called st_then_borrow_rejected_at_limit returns done
  ll_check("BorrowBook", "precondition_violated", "borrowing while already at the three-loan limit is rejected")
  return true
end

make a function called st_then_invariant_flagged_first returns done
  ll_check("BorrowBook", "invariant_violated_before", "a corrupted loan record is flagged before the operation is even considered")
  return true
end

# Deliberately WRONG claimed outcome: the loan count is claimed to stay
# the same after a successful borrow, which violates BorrowBook's own
# postcondition even though the precondition and invariant are both fine.
make a function called st_then_wrongly_claims_count_unchanged returns done
  let before_books = get("__vars", "LibraryLoans__books__before")
  schema_bind_state("LibraryLoans", "books", "after", before_books)
  let before_borrowed_by = get("__vars", "LibraryLoans__borrowedBy__before")
  schema_bind_state("LibraryLoans", "borrowedBy", "after", pmap_put(before_borrowed_by, "Dune", "A. Diallo"))
  let before_loan_count = get("__vars", "LibraryLoans__loanCount__before")
  schema_bind_state("LibraryLoans", "loanCount", "after", before_loan_count)
  ll_check("BorrowBook", "postcondition_violated", "a claimed loan count that doesn't actually increment is rejected")
  return true
end

make a function called st_then_return_accepted returns done
  let before_books = get("__vars", "LibraryLoans__books__before")
  schema_bind_state("LibraryLoans", "books", "after", before_books)
  let before_borrowed_by = get("__vars", "LibraryLoans__borrowedBy__before")
  schema_bind_state("LibraryLoans", "borrowedBy", "after", pmap_remove(before_borrowed_by, "Dune"))
  let before_loan_count = get("__vars", "LibraryLoans__loanCount__before")
  schema_bind_state("LibraryLoans", "loanCount", "after", pmap_put(before_loan_count, "S. Okonkwo", ll_loan_count_of(before_loan_count, "S. Okonkwo") - 1))
  ll_check("ReturnBook", "ok", "returning a borrowed title is accepted")
  return true
end

make a function called st_then_return_rejected_never_out returns done
  ll_check("ReturnBook", "precondition_violated", "returning a title nobody borrowed is rejected")
  return true
end

make a function called register_library_loans_steps returns done
  step("the library holds its standard catalogue", "st_given_standard_catalogue")
  step("no member has any books out", "st_given_no_loans_out")
  step("\"Dune\" is currently borrowed by \"S. Okonkwo\"", "st_given_dune_borrowed_by_okonkwo")
  step("\"A. Diallo\" already has three books out, at the loan limit", "st_given_diallo_at_loan_limit")
  step("the loan record incorrectly already shows \"A. Diallo\" with four loans", "st_given_corrupted_loan_record")
  step("\"A. Diallo\" borrows \"Foundation\"", "st_when_diallo_borrows_foundation")
  step("\"A. Diallo\" borrows \"Dune\"", "st_when_diallo_borrows_dune")
  step("\"S. Okonkwo\" returns \"Dune\"", "st_when_okonkwo_returns_dune")
  step("someone returns \"Foundation\"", "st_when_someone_returns_foundation")
  step("the loan is correctly recorded", "st_then_foundation_correctly_recorded")
  step("the borrow is rejected", "st_then_borrow_rejected_already_out")
  step("the borrow is rejected for being at the limit", "st_then_borrow_rejected_at_limit")
  step("the schema flags the corrupted record, not the borrow attempt", "st_then_invariant_flagged_first")
  step("the incorrect record is rejected", "st_then_wrongly_claims_count_unchanged")
  step("the return is accepted", "st_then_return_accepted")
  step("the return is rejected", "st_then_return_rejected_never_out")
  return true
end

make a function called library_loans_feature returns text
  return "Feature: Library loans, fully worked

Scenario: Borrowing an available title under the loan limit
  Given the library holds its standard catalogue
  And no member has any books out
  When \"A. Diallo\" borrows \"Foundation\"
  Then the loan is correctly recorded

Scenario: Borrowing a title someone else already has out
  Given the library holds its standard catalogue
  And \"Dune\" is currently borrowed by \"S. Okonkwo\"
  When \"A. Diallo\" borrows \"Dune\"
  Then the borrow is rejected

Scenario: Borrowing while already at the three-loan limit
  Given the library holds its standard catalogue
  And \"A. Diallo\" already has three books out, at the loan limit
  When \"A. Diallo\" borrows \"Dune\"
  Then the borrow is rejected for being at the limit

Scenario: A corrupted loan record is caught before the operation runs
  Given the library holds its standard catalogue
  And the loan record incorrectly already shows \"A. Diallo\" with four loans
  When \"A. Diallo\" borrows \"Foundation\"
  Then the schema flags the corrupted record, not the borrow attempt

Scenario: A scenario that under-reports its own effect is caught too
  Given the library holds its standard catalogue
  And no member has any books out
  When \"A. Diallo\" borrows \"Dune\"
  Then the incorrect record is rejected

Scenario: Returning a borrowed title
  Given the library holds its standard catalogue
  And \"Dune\" is currently borrowed by \"S. Okonkwo\"
  When \"S. Okonkwo\" returns \"Dune\"
  Then the return is accepted

Scenario: Returning a title nobody borrowed
  Given the library holds its standard catalogue
  And no member has any books out
  When someone returns \"Foundation\"
  Then the return is rejected
"
end

make a function called run_library_loans_schema_demo returns ok
  t_init()
  register_library_loans_schema()
  register_library_loans_steps()
  run_feature(library_loans_feature())
  t_report()
  return get("__vars", "t_fail") == 0
end

run_library_loans_schema_demo()

Compile and run in this browser

(not run yet)

The Negative Case: Catching a Scenario Before It Runs

RunRun 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: Three Operations and a Real Invariant

TheThe 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 every diagnosis schema_check can produce: 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

AA 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 examples below need real subprocess execution or a native-only host function, so they’re shown as source plus a real captured run rather than live in this page — see the callouts on each for exactly why.

Inductive Synthesis: A Logically Valid Rule, Still Policy-Violating

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 real logic engine, enumerates every value it proves true, and checks each one against a schema. Not runnable in this page’s sandbox: the induction engine’s own diagnosis step (synth5_induce → synth2_diagnose_hypothesis) verifies its candidate by spawning a real subprocess — confirmed directly by running it through the exact WASM binary above, which fails with exec_capture: ... operation not supported on this platform. That’s a real, structural limit of any browser sandbox, not a bug to fix.

  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

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 native function, plan_with_state, exposes that real resulting state directly — implemented three times over, honestly: as a Rust interpreter host function, in the Rust-to-native codegen path, and, canonically, as genuine self-hosted PatLang in self_hosting/lib/x64_runtime.patlang, compiled and run through the real patc1.exe --x64 production toolchain, not just the interpreter. Not runnable in this page’s sandbox: plan_with_state is brand new and isn’t in the WASM module embedded on this page yet.

  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 real three-step GOAP plan (pack for transit, ship to the depot, ship on to the destination); the schema checks the plan’s actual resulting facts — the book present at the destination and genuinely 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

CheckingChecking existing scenarios against a schema is the easier direction, and it’s the one that’s built. 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³. This direction remains unbuilt: require_fn/ensure_fn are always named, separately-compiled, introspectable functions rather than inlined text, specifically so a future generator could enumerate the operation registry without any rework to what’s here now.

What Was Actually Needed

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, 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. That’s precisely the harder problem Liu and Bowen’s PhD work spends its own length on, under Z refinement specifically. 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