From Scope to Spec

Overview

This page documents the transformation from Aimee's scope document to Anna's formal specification. This is the most critical handoff in GE's development pipeline. Every ambiguity that survives this transformation will propagate through tests, code, and into production.

CLIENT (human)
  → Faye/Sytske (Team PM — gathers requirements)
    → Aimee (Scope Architect — writes scope document)
      → Anna (Formal Specification — transforms to formal spec)
        → Antje (Test Generation — derives tests)
          → Developers (Implementation)

---

What a Scope Document Contains

Aimee's scope document is a functional specification written in business language. It answers the question: "What does the client want?"

Typical Scope Document Structure

Section	Content	Example
Problem Statement	What business problem does this solve?	"Clients cannot track their invoices"
User Stories	Who does what and why?	"As a business owner, I want to see all unpaid invoices so I can follow up"
Acceptance Criteria	When is this feature done?	"User can filter invoices by status, date range, and amount"
Data Requirements	What data is involved?	"Invoice has: number, amount, date, status, client reference"
Integration Points	What connects to what?	"Invoices sync with Exact Online accounting"
Non-Functional Requirements	Performance, security, availability	"Invoice list must load within 2 seconds"
Constraints	Business rules, regulations, limits	"Dutch VAT rules apply. Invoices are immutable after sending."
Open Questions	Unresolved items	"Should credit notes be separate entities or linked to invoices?"

What a Scope Document Does NOT Contain

• Implementation details (no "use PostgreSQL" or "implement with React")
• Formal invariants or pre/post-conditions
• Exhaustive edge cases
• Mathematical precision
• API contracts or data schemas

---

What a Formal Specification Contains

Anna's formal specification answers the question: "What MUST the system do, precisely?"

Formal Spec Structure (See Anna's Full Schema)

Section	Content	Source
Pre-conditions	What must be true before execution	Derived from scope constraints and business rules
Post-conditions	What must be true after execution	Derived from acceptance criteria
Invariants (min 3)	What must ALWAYS be true	Derived from business rules, data integrity, and safety
Edge Cases	Every boundary condition	Derived from data requirements + Anna's analysis
Examples	Concrete input/output pairs	Derived from user stories + edge cases
State Transitions	Valid state changes	Derived from workflow descriptions
Error Conditions	What happens when things fail	Derived from constraints + Anna's analysis
Constitution Compliance	GE principle alignment	Verified against constitution

---

The Transformation Process

Step 1: Read and Decompose the Scope

Anna reads the entire scope document and decomposes it into discrete functions or features.

CHECK: Can each function/feature be specified independently? IF: Yes — proceed with one spec per function IF: No — functions are coupled THEN: Specify the coupled group together, noting the coupling explicitly

RULE: One formal spec per function/feature. Never combine unrelated functions. RULE: Maximum 15,000 tokens per spec. Split if larger.

Step 2: Disambiguation

This is the most critical step. Anna systematically identifies every ambiguous element.

Ambiguity Categories

1. Vague Quantifiers

Scope Says	Anna Asks	Resolution
"large orders"	"Define 'large' — item count, total amount, or both?"	Aimee defines: "> 100 items OR > $10,000"
"quickly"	"Define maximum response time in milliseconds"	Aimee defines: "< 2000ms at p95"
"many users"	"Define concurrent user count"	Aimee defines: "Up to 500 simultaneous"
"reasonable"	Not acceptable — remove or quantify	Aimee replaces with specific value

2. Missing Boundaries

CHECK: Does the scope define minimum AND maximum for every numeric field? IF: Only maximum defined — what happens at minimum (0, empty, null)? IF: Only minimum defined — what is the system limit? IF: Neither defined — STOP. Ask Aimee.

SCOPE: "Users can upload documents"
ANNA ASKS:
  - Minimum file size? (0 bytes? 1 byte?)
  - Maximum file size? (10MB? 100MB? Unlimited?)
  - Allowed file types? (All? Specific list?)
  - What happens at the boundary? (Exactly 10MB — accept or reject?)
  - What happens above the boundary? (Error message? Silent truncation?)

3. Undefined Error Behavior

CHECK: For every operation in the scope, does the scope define what happens when it fails? IF: No failure behavior defined — Anna asks Aimee: - What if the database is unavailable? - What if the external API returns an error? - What if the request times out? - What if input validation fails? - What if the user's session expires mid-operation?

4. Implicit Assumptions

CHECK: Does the scope assume knowledge that is not stated?

SCOPE: "The system applies the correct tax rate"
IMPLICIT ASSUMPTIONS:
  - Which country's tax rules? (Netherlands, but which rates?)
  - Does the rate depend on product category? (Yes — 0%, 9%, 21% in NL)
  - When does a rate change take effect? (Date of invoice? Date of delivery?)
  - What about cross-border transactions?
ANNA: Makes each assumption explicit in the spec or asks Aimee.

5. Conflicting Requirements

CHECK: Do any scope elements contradict each other?

SCOPE: "Invoices are immutable after sending" + "Users can edit the amount on any invoice"
CONFLICT: An immutable invoice cannot have its amount edited.
ANNA: Escalates to Aimee. Aimee clarifies with client.

Decision Tree: Disambiguation

FOR each scope element:
  CHECK: Is it measurable and testable as written?
    IF: Yes → proceed to formalization
    IF: No → identify ambiguity type
      CHECK: Can Anna resolve it from context in the scope document?
        IF: Yes → resolve and document the resolution
        IF: No → escalate to Aimee
          CHECK: Can Aimee resolve from client knowledge?
            IF: Yes → Aimee provides clarification → Anna updates
            IF: No → Aimee asks the client via Faye/Sytske
              CHECK: Client responds?
                IF: Yes → resolution flows back through chain
                IF: No → feature is blocked. Anna does NOT proceed.

RULE: Anna NEVER guesses. Every resolution is either documented in the scope or explicitly confirmed by Aimee.

---

Step 3: Edge Case Enumeration

After disambiguation, Anna systematically enumerates edge cases for each function.

Edge Case Generation Method

For each input parameter: 1. Zero/empty — What if this input is 0, empty string, empty array, null? 2. One — What if this input has exactly one element? 3. Boundary — What if this input is exactly at the minimum or maximum allowed value? 4. Boundary +/- 1 — What about values just inside and just outside the boundary? 5. Maximum — What if this input is at the system limit? 6. Invalid type — What if this input is the wrong type? 7. Malicious — What if this input is a SQL injection, XSS payload, or path traversal?

For each state transition: 1. Already in target state — What if we try to transition to the current state? 2. Invalid transition — What if we try an impossible transition? 3. Concurrent transition — What if two transitions happen simultaneously? 4. Interrupted transition — What if the system crashes mid-transition?

For each external dependency: 1. Unavailable — What if the dependency is down? 2. Slow — What if the dependency responds after timeout? 3. Invalid response — What if the dependency returns unexpected data? 4. Partial success — What if the dependency succeeds partially?

---

Step 4: State Machine Extraction

Many features involve entities that transition between states. Anna extracts these into explicit state machines.

Method

1. Identify all states mentioned in the scope (explicitly and implicitly)
2. Identify all transitions (actions that change state)
3. Identify guards (conditions that must be true for a transition)
4. Identify side effects of each transition
5. Verify completeness — every state has at least one outgoing transition or is a terminal state

Example

Scope says: "Invoices start as drafts. They can be sent to the client. Once sent, the client can pay or dispute them. Paid invoices are archived."

Anna extracts:

state_machine:
  entity: Invoice
  states: [draft, sent, paid, disputed, archived, cancelled]
  transitions:
    - from: draft
      to: sent
      action: send
      guard: "invoice.amount > 0 AND invoice.recipient IS NOT NULL"
      side_effects: ["email sent to recipient", "sent_at timestamp set"]
    - from: draft
      to: cancelled
      action: cancel
      guard: none
      side_effects: ["cancelled_at timestamp set"]
    - from: sent
      to: paid
      action: record_payment
      guard: "payment.amount == invoice.amount"
      side_effects: ["paid_at timestamp set", "payment record created"]
    - from: sent
      to: disputed
      action: dispute
      guard: "dispute.reason IS NOT NULL"
      side_effects: ["disputed_at timestamp set", "dispute notification sent"]
    - from: disputed
      to: sent
      action: resolve_dispute
      guard: "resolution IS NOT NULL"
      side_effects: ["dispute resolved notification sent"]
    - from: paid
      to: archived
      action: archive
      guard: "paid_at < 30 days ago"
      side_effects: ["archived_at timestamp set"]
  terminal_states: [archived, cancelled]
  initial_state: draft

CHECK: Is every state reachable from the initial state? CHECK: Does every non-terminal state have at least one outgoing transition? CHECK: Are there any implicit states not mentioned in the scope?

---

Step 5: Data Model Derivation

Anna derives a precise data model from the scope requirements.

Method

1. Identify all entities mentioned in the scope
2. For each entity, identify all attributes (explicitly mentioned and implied)
3. Define types, constraints, and relationships
4. Define validation rules
5. Define uniqueness constraints
6. Define cascading behavior (what happens when a parent is deleted?)

Example

data_model:
  Invoice:
    attributes:
      id:
        type: string
        format: "INV-{YYYYMMDD}-{sequential}"
        unique: true
        immutable: true
      amount:
        type: decimal
        precision: 2
        min: 0.01
        max: 999999.99
        immutable_after: sent
      status:
        type: enum
        values: [draft, sent, paid, disputed, archived, cancelled]
        default: draft
      recipient_email:
        type: string
        format: email
        required_before: sent
      created_at:
        type: timestamp
        auto: true
        immutable: true
    relationships:
      - entity: Client
        type: belongs_to
        required: true
        on_delete: restrict
      - entity: LineItem
        type: has_many
        min: 1
        on_delete: cascade

---

Step 6: API Contract Definition

If the feature involves API endpoints, Anna defines the contract.

api_contract:
  endpoint: "POST /api/invoices"
  method: POST
  authentication: required
  authorization: "invoicing.create"

  request:
    content_type: application/json
    body:
      clientId:
        type: string
        required: true
      lineItems:
        type: array
        min_length: 1
        items:
          description: { type: string, required: true, max_length: 200 }
          amount: { type: decimal, required: true, min: 0.01 }
          quantity: { type: integer, required: true, min: 1 }

  responses:
    201:
      body: { id: string, status: "draft", amount: decimal, createdAt: timestamp }
    400:
      body: { error: string, field: string }
      when: "Validation fails"
    401:
      body: { error: "Unauthorized" }
      when: "No valid session"
    403:
      body: { error: "Forbidden" }
      when: "User lacks invoicing.create permission"
    409:
      body: { error: "Duplicate", existingId: string }
      when: "Idempotency key matches existing invoice"

  idempotency:
    key_header: "Idempotency-Key"
    behavior: "Return existing resource if key matches"
    window: "24 hours"

---

Step 7: The "No Ambiguity" Rule

Before publishing, Anna performs a final ambiguity check:

FOR each statement in the formal spec:
  CHECK: Can this statement be interpreted in exactly one way?
    IF: Yes → keep
    IF: No → revise until unambiguous
  CHECK: Can this statement be tested by an automated test?
    IF: Yes → keep
    IF: No → revise until testable
  CHECK: Does this statement use any of these forbidden words?
    - "appropriate" → replace with specific criteria
    - "reasonable" → replace with specific threshold
    - "as needed" → replace with specific condition
    - "etc." → enumerate all items
    - "should" → replace with "must" or remove
    - "may" → replace with "must" or define when
    - "generally" → replace with specific rule
    IF: Yes → revise

RULE: The formal spec uses "MUST," "MUST NOT," "SHALL," and "SHALL NOT" per RFC 2119. Never "should" or "may."

---

Error Handling: When Aimee's Scope Is Incomplete

IF: The scope document has open questions (common — Aimee often flags these) THEN: Anna addresses each open question: - Can the question be answered from the scope context? → Anna resolves and documents - Is the question a business decision? → Anna escalates to Aimee → Aimee escalates to Faye/Sytske → client - Is the question a technical decision? → Anna escalates to Aimee with options and tradeoffs

IF: The scope document is missing a section entirely THEN: Anna escalates to Aimee listing what is missing. Anna does NOT fill in gaps with assumptions.

IF: Aimee and client cannot agree on a requirement THEN: The feature is blocked. Anna does not produce a spec for blocked features.

RULE: A blocked feature with no spec is better than a shipped feature with wrong spec.

---

Traceability Requirements

Every element in the formal spec must trace back to the scope document:

lineage:
  functional_spec_id: "SCOPE-2026-0326-INV-001"
  functional_spec_path: "wiki/docs/clients/acme/scoping/invoicing-v2.md"
  derived_from: "Section 3.2 — Invoice Creation"
  ambiguity_resolutions:
    - question: "What is the maximum invoice amount?"
      resolution: "999,999.99 EUR — confirmed by client 2026-03-25"
      resolved_by: aimee
    - question: "Are partial payments allowed?"
      resolution: "No — full payment only in v1. Partial payments deferred to v2."
      resolved_by: client

RULE: If a formal spec element cannot be traced to a scope element, it is either speculative (remove it) or reveals a scope gap (report to Aimee).

---

Related Documentation

• Formal Specification Philosophy — Why GE specifies formally
• Spec-Driven Testing — How specs feed test generation
• Formal Specification Pitfalls — Common mistakes in specification
• TDD Workflow — Full pipeline including specification stage
• Anna Agent — Agent details and schema