DOMAIN:REQUIREMENTS:FORMAL_SPECIFICATION¶

OWNER: anna (Formal Specification Agent) UPDATED: 2026-03-24 SCOPE: transforming functional specs into unambiguous formal specifications PREREQUISITE: scope-architecture.md (Aimee's functional spec must exist)

PRINCIPLE: AMBIGUITY_IS_A_BUG¶

RULE: if two developers could interpret a requirement differently, the spec has a bug. RULE: formal specs use precise language with defined terms. No synonyms, no pronouns, no assumptions. RULE: every requirement has a unique ID, testable acceptance criteria, and defined edge cases. REASON: agents execute literally. A human developer might "figure out what was meant." An agent implements exactly what was written. Ambiguity becomes a code defect every single time.

ANNA_INPUT: THE_FUNCTIONAL_SPEC¶

Anna receives Aimee's functional specification containing: - Feature list with acceptance criteria (Given-When-Then) - User roles and permissions - Data model overview - Cross-cutting concerns - Non-functional requirements

ANNA_FIRST_ACTION: AMBIGUITY_SCAN¶

Read the entire functional spec. Flag every instance of:

AMBIGUITY_MARKERS (flag on sight):
- "appropriate" → appropriate for whom? Define the rule.
- "relevant" → relevant by what criteria? List them.
- "should" → must or must not. Pick one.
- "etc." → enumerate every item. No et cetera in specs.
- "similar" → identical to what? Define the comparison.
- "intuitive" → what specific interaction? Define it.
- "user-friendly" → what specific UX patterns? Define them.
- "fast" → what response time in milliseconds? Define it.
- "secure" → what specific security measures? List them.
- "handle gracefully" → what specific error behavior? Define it.
- "as needed" → when specifically? Define the trigger condition.
- "standard" → which standard? ISO, RFC, internal? Cite it.

EACH_FLAG: send back to Aimee with a specific question. Do not proceed with ambiguity.

REQUIREMENT_ID_SCHEME¶

FORMAT: REQ-{feature_number}-{sequential}

EXAMPLES:
REQ-001-001: User registration with email and password
REQ-001-002: Email validation with confirmation link
REQ-001-003: Password strength requirements
REQ-002-001: Order creation with client selection
REQ-002-002: Order line item management
REQ-002-003: Order total calculation with tax

GROUPING: first three digits match feature number (F-001 → REQ-001-xxx)
TRACEABILITY: every WP references REQ IDs. Every test references REQ IDs.
COVERAGE: no REQ may exist without at least one test and one WP.

FORMAL_SPEC_STRUCTURE¶

REQUIREMENT_TEMPLATE¶

### REQ-{nnn}-{nnn}: {Title}

**Source:** F-{nnn} ({feature name from Aimee's spec})

**Description:**
{Precise, unambiguous description of what the system must do.
 Uses defined terms from the glossary. No pronouns.
 Every noun refers to a specific entity. Every verb is a specific action.}

**Preconditions:**
- {Condition that must be true before this requirement applies}
- {Another precondition}

**Postconditions:**
- {Condition that must be true after this requirement is fulfilled}
- {Another postcondition}

**Invariants:**
- {Condition that must remain true throughout execution}

**Acceptance Criteria:**
- AC-1: GIVEN {state} WHEN {action} THEN {result}
- AC-2: GIVEN {state} WHEN {action} THEN {result}

**Edge Cases:**
- EC-1: WHEN {unusual condition} THEN {expected behavior}
- EC-2: WHEN {boundary condition} THEN {expected behavior}

**Error Conditions:**
- ERR-1: WHEN {invalid input/state} THEN {error response with code}
- ERR-2: WHEN {system failure} THEN {fallback behavior}

EXAMPLE_FORMAL_REQUIREMENT¶

### REQ-002-003: Order Total Calculation

**Source:** F-001 (Order Creation)

**Description:**
The system must compute the order total as the sum of all line item
subtotals. Each line item subtotal equals the product of the line item
quantity and the line item unit price, multiplied by (1 + the line item
tax rate). The order total is stored as a decimal with 2 decimal places,
rounded half-up.

**Preconditions:**
- The order exists in the database
- The order contains at least one line item
- Each line item has: quantity (positive integer), unit_price (non-negative
  decimal, 2 decimal places), tax_rate (decimal between 0.00 and 1.00)

**Postconditions:**
- order.total = sum of (line_item.quantity * line_item.unit_price *
  (1 + line_item.tax_rate)) for all line items, rounded to 2 decimal places
- order.total_ex_tax = sum of (line_item.quantity * line_item.unit_price)
  for all line items, rounded to 2 decimal places
- order.total_tax = order.total - order.total_ex_tax

**Invariants:**
- order.total >= 0
- order.total >= order.total_ex_tax
- order.total_tax >= 0
- order.total == order.total_ex_tax + order.total_tax

**Acceptance Criteria:**
- AC-1: GIVEN an order with 1 line item (qty=2, price=10.00, tax=0.21)
  WHEN total is calculated
  THEN order.total = 24.20, order.total_ex_tax = 20.00, order.total_tax = 4.20

- AC-2: GIVEN an order with 2 line items (qty=1,price=100.00,tax=0.21)
  and (qty=3,price=5.50,tax=0.09)
  WHEN total is calculated
  THEN order.total = 100*1.21 + 3*5.50*1.09 = 121.00 + 17.99 = 138.99

- AC-3: GIVEN an order with 0 line items
  WHEN total is calculated
  THEN order.total = 0.00

**Edge Cases:**
- EC-1: WHEN line_item.unit_price = 0.00 THEN line item subtotal = 0.00
  (free items are valid)
- EC-2: WHEN line_item.tax_rate = 0.00 THEN no tax applied to that line
  item (tax-exempt products)
- EC-3: WHEN calculation produces more than 2 decimal places THEN round
  half-up (e.g., 10.005 → 10.01)
- EC-4: WHEN order has maximum line items (50) THEN calculation completes
  within 100ms

**Error Conditions:**
- ERR-1: WHEN line_item.quantity <= 0 THEN reject with validation error
  code INVALID_QUANTITY, message "Quantity must be a positive integer"
- ERR-2: WHEN line_item.unit_price < 0 THEN reject with validation error
  code INVALID_PRICE, message "Price must be non-negative"
- ERR-3: WHEN line_item.tax_rate < 0 or > 1 THEN reject with validation
  error code INVALID_TAX_RATE, message "Tax rate must be between 0% and 100%"

INVARIANT_DEFINITION¶

WHAT_IS_AN_INVARIANT¶

An invariant is a condition that must be true at ALL times, not just before/after a specific action. Invariants are the strongest form of requirement.

SYSTEM_INVARIANTS¶

## System-Wide Invariants

INV-001: Every order belongs to exactly one client.
         order.client_id references an existing client record.

INV-002: Order status follows the defined state machine.
         No order may transition to a state not defined in the state machine.

INV-003: Order total always equals the computed sum of line items.
         Modifying a line item triggers recalculation. No stale totals.

INV-004: No negative quantities, prices, or totals exist in the database.
         Database constraints enforce this at the column level.

INV-005: Every user action is attributable.
         Every create/update/delete has a user_id and timestamp in the audit log.

INV-006: Soft-deleted records are invisible to application queries.
         deleted_at IS NOT NULL excludes the record from all queries.

INVARIANT_RULES¶

RULE: invariants are implemented as database constraints where possible. RULE: invariants that cannot be database constraints must be application-level checks. RULE: invariants are tested by the TDD suite — Antje writes invariant tests. RULE: every invariant has an ID (INV-nnn) for traceability.

PRE_AND_POST_CONDITIONS¶

FORMAT¶

PRECONDITION: a condition that must be true BEFORE an operation executes.
              If false, the operation must not proceed.

POSTCONDITION: a condition that must be true AFTER an operation completes.
               If false, the operation has a bug.

EXAMPLE_FOR_ORDER_CREATION¶

## Operation: Create Order

PRECONDITIONS:
- PRE-1: Authenticated user with role STAFF or ADMIN
- PRE-2: Client identified by client_id exists and is not soft-deleted
- PRE-3: At least one line item provided
- PRE-4: All line items have valid quantity (>0), price (>=0), tax_rate (0-1)
- PRE-5: Total line items <= 50

POSTCONDITIONS:
- POST-1: New order record exists with status = DRAFT
- POST-2: order.order_number is auto-generated and unique
- POST-3: order.created_by = authenticated user ID
- POST-4: order.created_at = current timestamp
- POST-5: All line items are persisted with correct order_id FK
- POST-6: order.total is calculated correctly (per REQ-002-003)
- POST-7: Audit log entry created: action=ORDER_CREATED, entity_id=order.id

STATE_MACHINE_MODELING¶

WHEN_TO_USE¶

Use state machines for any entity with a status field that has rules about transitions.

FORMAT: MERMAID_STATE_DIAGRAM¶

## Order State Machine

```mermaid
stateDiagram-v2
    [*] --> Draft: create order
    Draft --> Submitted: submit (staff)
    Draft --> Cancelled: cancel (staff)
    Submitted --> InProgress: start work (staff)
    Submitted --> Draft: return to draft (staff)
    Submitted --> Cancelled: cancel (staff/admin)
    InProgress --> Completed: mark complete (staff)
    InProgress --> Submitted: pause (staff)
    InProgress --> Cancelled: cancel (admin only)
    Completed --> Invoiced: generate invoice (admin)
    Completed --> InProgress: reopen (admin)
    Invoiced --> Archived: archive (admin)
    Cancelled --> [*]
    Archived --> [*]
```

STATE_MACHINE_SPECIFICATION¶

## Order Status Transitions

| From        | To          | Trigger             | Guard Condition          | Side Effects                  |
|-------------|-------------|---------------------|--------------------------|-------------------------------|
| -           | Draft       | Create order        | Valid line items         | Generate order number          |
| Draft       | Submitted   | Staff clicks Submit | At least 1 line item     | Notify assigned staff          |
| Draft       | Cancelled   | Staff clicks Cancel | -                        | Audit log: cancelled           |
| Submitted   | InProgress  | Staff clicks Start  | Staff is assigned        | Set started_at timestamp       |
| Submitted   | Draft       | Staff clicks Return | -                        | Clear submitted_at             |
| Submitted   | Cancelled   | Staff/Admin cancel  | -                        | Notify client if portal active |
| InProgress  | Completed   | Staff clicks Done   | All items fulfilled      | Set completed_at               |
| InProgress  | Submitted   | Staff clicks Pause  | -                        | Clear started_at               |
| InProgress  | Cancelled   | Admin only          | -                        | Audit log: admin cancelled     |
| Completed   | Invoiced    | Admin gen invoice   | Invoice system available | Create invoice record          |
| Completed   | InProgress  | Admin reopens       | -                        | Audit log: reopened            |
| Invoiced    | Archived    | Admin archives      | Invoice is paid          | Set archived_at                |

TERMINAL STATES: Cancelled, Archived (no transitions out)
GUARD: if guard condition is not met, transition is rejected with descriptive error
SIDE EFFECTS: happen atomically with the transition (same DB transaction)

STATE_MACHINE_RULES¶

RULE: every state is reachable from the initial state. RULE: every non-terminal state has at least one outgoing transition. RULE: terminal states have zero outgoing transitions. RULE: every transition has a trigger (what causes it) and optionally a guard (what prevents it). RULE: side effects of transitions are documented and atomic. RULE: the state machine is the source of truth for status changes. Application code must not set status directly — it must invoke a transition.

API_CONTRACT_SPECIFICATION¶

FORMAT¶

Anna specifies API contracts at the level of request/response schemas, not implementation.

### API: POST /api/orders

**Purpose:** Create a new order

**Authentication:** Required. Roles: STAFF, ADMIN

**Request Body:**
```typescript
{
  client_id: string;         // UUID of existing client
  notes?: string;            // Optional order notes, max 1000 chars
  line_items: Array<{
    description: string;     // Product/service description, max 200 chars
    quantity: number;         // Positive integer
    unit_price: number;      // Non-negative, 2 decimal places
    tax_rate: number;        // Decimal 0.00-1.00
  }>;                        // 1-50 items required
}
```

**Success Response (201):**
```typescript
{
  success: true;
  data: {
    id: string;              // UUID
    order_number: string;    // "ORD-2026-00001" format
    status: "draft";
    client_id: string;
    line_items: Array<{...}>; // As submitted, with computed subtotals
    total: number;
    total_ex_tax: number;
    total_tax: number;
    created_by: string;      // User UUID
    created_at: string;      // ISO 8601
  };
}
```

**Error Responses:**
- 400 VALIDATION_ERROR: Invalid input (Zod validation failed)
- 401 UNAUTHORIZED: Not authenticated
- 403 FORBIDDEN: User role not STAFF or ADMIN
- 404 NOT_FOUND: client_id does not exist
- 422 BUSINESS_RULE_ERROR: Line items empty or exceed 50

EDGE_CASE_ENUMERATION¶

EDGE_CASE_CATEGORIES¶

CATEGORY_1: BOUNDARY_VALUES — min and max values for every numeric field CATEGORY_2: EMPTY_STATES — what happens when lists are empty, strings are blank CATEGORY_3: CONCURRENT_OPERATIONS — two users modify the same record CATEGORY_4: TIMING — what happens at midnight (date boundaries), during deployment CATEGORY_5: DATA_INTEGRITY — referential integrity when related records are deleted CATEGORY_6: PERMISSION_BOUNDARIES — what happens at the edge of role permissions CATEGORY_7: UNICODE — non-ASCII characters in text fields CATEGORY_8: NETWORK — slow connections, timeouts, retry behavior

EDGE_CASE_TEMPLATE¶

## Edge Cases: F-001 Order Creation

| ID     | Category    | Condition                              | Expected Behavior                          |
|--------|-------------|----------------------------------------|--------------------------------------------|
| EC-001 | Boundary    | quantity = 1 (minimum)                 | Accepted, subtotal = unit_price * (1+tax)  |
| EC-002 | Boundary    | quantity = 999999 (very large)         | Accepted if integer, total computed         |
| EC-003 | Boundary    | unit_price = 0.00                      | Accepted (free item), subtotal = 0.00      |
| EC-004 | Boundary    | unit_price = 99999.99                  | Accepted, total computed                   |
| EC-005 | Boundary    | line_items count = 1 (minimum)         | Accepted                                   |
| EC-006 | Boundary    | line_items count = 50 (maximum)        | Accepted                                   |
| EC-007 | Boundary    | line_items count = 51                  | Rejected: BUSINESS_RULE_ERROR              |
| EC-008 | Empty       | notes = "" (empty string)              | Accepted, stored as null                   |
| EC-009 | Empty       | notes = null (omitted)                 | Accepted, stored as null                   |
| EC-010 | Concurrent  | Two users create order for same client | Both succeed with unique order numbers     |
| EC-011 | Concurrent  | User submits order twice (double-click)| Idempotent: second request returns first   |
| EC-012 | Integrity   | client is soft-deleted after form load | Reject on submit: client NOT_FOUND         |
| EC-013 | Unicode     | description contains emoji/CJK chars   | Accepted, stored and displayed correctly   |
| EC-014 | Unicode     | description contains SQL injection      | Parameterized query prevents execution     |
| EC-015 | Permission  | VIEWER role tries to create order      | Rejected: FORBIDDEN                        |

WHAT_MAKES_A_SPEC_IMPLEMENTABLE¶

THE_IMPLEMENTABILITY_TEST¶

A spec is implementable if an agent can read it and produce working code WITHOUT asking any questions.

CHECKLIST:

[ ] Every input field has: name, type, constraints (min, max, required, format)
[ ] Every output field has: name, type, how it is computed or where it comes from
[ ] Every status has: defined transitions, guard conditions, side effects
[ ] Every API endpoint has: method, path, auth, request schema, response schema, error codes
[ ] Every error has: when it occurs, what error code, what message
[ ] Every business rule has: when it applies, what it does, what happens if violated
[ ] No requirement references another requirement ambiguously ("see above" is banned)
[ ] Every term used has a definition in the glossary or is self-evident

FORMAL_SPEC_QUALITY_GATE¶

Before Anna submits to the gate:

COMPLETENESS:
[ ] Every functional requirement from Aimee's spec has a REQ-nnn-nnn ID
[ ] Every REQ has preconditions, postconditions, and acceptance criteria
[ ] Every entity with a status field has a state machine
[ ] Every API endpoint has a contract
[ ] Edge cases are enumerated for every input feature
[ ] Error conditions are specified for every endpoint

PRECISION:
[ ] No ambiguity markers remain (should, might, appropriate, etc.)
[ ] All numeric constraints are exact
[ ] All string constraints have max lengths
[ ] All enums are fully listed (not "such as" or "including")
[ ] All date/time formats are specified (ISO 8601)

CONSISTENCY:
[ ] Field names are identical across spec, API contracts, and data model
[ ] Status names match between state machines and API responses
[ ] Error codes are unique and consistently structured
[ ] REQ numbering is sequential within each feature

TRACEABILITY:
[ ] Every REQ traces to an Aimee feature (F-nnn)
[ ] Traceability is bidirectional (feature → reqs, req → feature)
[ ] Invariants are numbered and traceable

COLLABORATION_WITH_DOWNSTREAM_AGENTS¶

TO_ANTJE (TDD)¶

Anna's spec is Antje's input for TDD test specifications. Antje reads: - Acceptance criteria → become test cases - Edge cases → become boundary tests - Error conditions → become negative test cases - Invariants → become property-based tests

TO_ALEXANDER (DESIGN)¶

Anna's spec tells Alexander: - What screens exist (from features and their acceptance criteria) - What data is displayed (from API response schemas) - What user interactions exist (from state transitions and forms) - What error states to design for (from error conditions)

TO_FAYE/SYTSKE (PM)¶

Anna's spec tells the PM: - How many REQs exist (determines WP count) - Which REQs depend on each other (from preconditions referencing other REQs) - Which REQs are complex (many edge cases = larger WP) - Which REQs are independent (no cross-references = parallelizable)