Examples and scenarios

Examples and scenarios

Examples turn a promise into concrete inputs, actions and observations. Keep the expected result visible; put application mechanics in the generated driver implementation.

A readable shopping scenario

main.expec

examples {
  setup bookIsAvailable(title: Text) returns Nothing
  setup startWithEmptyBasket() returns Nothing
  action addBook(title: Text) returns Nothing
  observation bookQuantity(title: Text) returns Number
  check expectBookQuantity(title: Text, expected: Number) {
    let actual = bookQuantity(title)
    assert actual == expected
  }
  scenario "a shopper can add an available book" {
    given bookIsAvailable("Dune")
    given startWithEmptyBasket()
    when addBook("Dune")
    then expectBookQuantity("Dune", 1)
  }
}

setup prepares state. action requests behavior. observation reads the actual application. check compares that observation with an independently authored expectation.

The bodyless runtime operations above are contracts. Generated driver stubs remain unfinished until you implement them against the real application. The quantity must come from that application, not from a helper that guesses what the preceding calls should have done. The released README supplies a complete application/driver journey with wrong behavior, failure and repair.

Scenario order and roles

A scenario has zero or more given steps, one or more when steps, then one or more then steps, in that order.

• given calls a setup operation or an applicable function/capability contract.
• when calls an action or applicable callable contract.
• then calls a check, evaluates a Boolean condition, or states a prose obligation.
• An observation alone returning Number is not a Boolean expectation. Compare it to a number or pass it to a check.
• Do not use an action for preparation or an observation as the action.

Capture a result

main.expec

type Basket {
  id: Text
}
examples {
  action startBasket() returns Basket
  observation quantity(basket: Basket) returns Number
  scenario "a new basket is empty" {
    when basket = startBasket()
    then quantity(basket) == 0
  }
}

A given or when step can bind its result using name = call(...). Later steps in that scenario can use the capture. Captures are ordered, unique and local to one scenario. You cannot capture Nothing or treat an unspecified result as a known value.

Fixtures

A fixture is typed reusable example data. Give it a type and compatible explicit values. Supply every nonoptional field even if its type declares a default; fixture checking does not evaluate or inherit those defaults. An optional field may be omitted without consuming its default.

main.expec

type Book {
  title: Text
  available: Boolean = true
}
examples {
  fixture dune: Book = Book { title: "Dune", available: true }
  fixture openingStock: List<Book> = [dune]
  example "fixture title": dune.title => "Dune"
}

Fixture values describe data; runtime calls are rejected even when nested inside a record or list. Use setup for real state preparation. Cyclic fixtures or values of incompatible types are errors.

Reusable helpers and checks

Helper bodies contain ordered let, do and return statements. Check bodies use let, do and assert, and must contain an assertion when a body is supplied. An assertion accepts a Boolean expression or another check call. Checks cannot return values or be invoked as an effect with do. Use do for an actual runtime call, not a bare value.

main.expec

examples {
  action addBook(title: Text) returns Nothing
  action addTwoBooks(title: Text) returns Nothing {
    do addBook(title)
    do addBook(title)
  }
  observation double(value: Number) returns Number {
    let doubled = value * 2
    return doubled
  }
  check expectDouble(value: Number, expected: Number) {
    let actual = double(value)
    assert actual == expected
  }
}

This block defines reusable composition and an arithmetic check; it declares no scenario about basket behavior. A real basket check must observe basket state as in the first example.

Locals exist after their declaration and do not cross helper bodies. A value-producing body must return a compatible value; statements after a return are invalid. A Nothing helper cannot return a value. A check has no returns clause; its assertions are expectations. A bodyless operation remains an implementation obligation. An explicitly empty Nothing helper body describes a deliberate no-op; an empty check is rejected because it verifies nothing.

Short examples

main.expec

function multiply(a: Number, b: Number) returns Number
examples for multiply {
  example "eight times eight": multiply(8, 8) => 64
}

example "title": actual => expected compares one expression with a concrete expected value. The expected value is independently authored, not calculated by inspecting the implementation. Here the function is still unimplemented.

Prose needs verification

main.expec

function title() returns Text
examples for title {
  example "literal text": title() => "Dune"
  example "descriptive title": title() => satisfies "Describe the title clearly."
}

"Dune" is a literal expected Text value. satisfies "…" is not an executable assertion: it records an unfinished verification obligation. A checked file can retain that obligation without claiming that the behavior passed.

Attach examples to a subject

An ownerless examples { ... } block can describe independent test operations. examples for StoreGame { ... } gives it an explicit subject. An inline examples block inside a concept uses that owner as its subject.

main.expec

concept StoreGame {
  capability save(snapshot: Text) returns Nothing
  examples {
    scenario "save a snapshot" {
      when save("current")
      then satisfies "The snapshot is stored."
    }
  }
}

Helpers and fixtures belong to their examples block; one block does not automatically borrow helpers from another. To move examples into another file, use examples attachments.

Related: Expressions and operators · Capabilities and contracts · Output support