Write a specification

This guide covers authoring an Executable System Specification. The normative example is examples/billing/ in the repository — deliberately the smallest system that exercises the core of the model. Concepts are covered in ESS; these pages are about writing one.

Pages in this guide

1. Lay out and validate a specification — the files, where generated output goes, reading refusals, checking what resolved, and names.
2. Refusals, fields and invariants — what the model insists on: declared outcomes, invariants, enums, instants, text, JSON and Binary64 fields.
3. Guards and outcome selection — choosing an outcome from input, held state or stored fields.
4. Commands and outcomes — wrong-state answers, unknown instances, existence, filters, deletion and event value sources.
5. Values and credentials — value expressions and the caller's credential; Views — view consistency, paging and aggregates.
6. Components and bindings — the layers above the domains and bindings between components.
7. Selections, periodic causes and delivery context — what a binding reads besides its event payload, and clock-reading provenance.
8. Conversions and wire names — conversions between contexts, wire spellings and error wire codes.

Where each section went

This guide used to be a single page. Each of its sections is listed here under its old anchor, so an older link still finds it.

• Layout
• Keep sources and generated output together
• Name the ess release the specification is maintained with
• Validate early, read the refusals
• What the model insists on
• A command that can be refused says so
• An invariant reads only what every creation sets
• Cover every declared enum value
• Order two instants
• Say which characters a text may hold, and how long it may be
• Say what a text starts with
• Carry any JSON value
• Carry finite binary floating-point values
• Select an outcome from the held subject state
• Guard an outcome by the subject's stored fields
• An outcome the input cannot decide says that too
• One outcome for many commands
• Illegal lifecycle moves are illegal by absence
• A command says what it answers when invoked in the wrong state
• An unknown instance can have its own outcome
• A request with no input can have its own outcome
• An outcome can be selected by whether the record exists
• An outcome can change every record a filter selects
• An outcome can delete its subject
• A creation can land in a declared state
• An accepted request can change nothing
• A system can run inside ambient preconditions
• An event's values need a declared source
• Value expressions
• Read the caller's credential
• An input refused when absent is present afterwards
• A view declares its consistency
• A view can be paged
• Aggregate views
• A binding says what happens when it fails
• Bound a retry
• Read a field inside an event envelope
• Select ordered records in a binding
• Declare a periodic host cause
• Read the channel an event arrived on
• Preserve clock-reading provenance
• Crossing contexts takes a declared conversion
• An enum variant can carry its own wire spelling
• A field can carry its own wire name
• Say whether an absent Optional is sent as null
• Three layers above the domains
• Check what you just wrote resolved
• Names

Next

• Verify an implementation — generate the suite this specification obliges, run it, and turn the result into evidence.
• The billing example — the billing example's source next to its generated output.