partition

/z-spec:partition - Derive Test Cases from Z Specification

Apply Test Template Framework (TTF) tactics to operation schemas in a Z specification to produce a complete partition table of test cases. Each partition represents a distinct behavioral class that must be tested to verify the implementation conforms to the spec.

Input

Arguments: $ARGUMENTS

Parse arguments:

• First positional argument: Z specification file (default: search docs/*.tex)
• --code [language]: Generate executable test code (auto-detect language if omitted)
• --operation=NAME: Partition a single operation (default: all operations)
• --json: Output partition data as JSON instead of markdown

Process

0. Prerequisites

This command requires no external tools. It reads an existing Z specification and applies testing tactics analytically. The specification should already exist and have been type-checked (via /z-spec:check).

1. Locate the Specification

If a file path is provided, use it directly.

If no file specified:

• Look in docs/ for .tex files containing Z specifications
• If multiple found, ask user to specify

Read the specification file.

2. Extract Operation Schemas

Scan the specification for operation schemas. An operation schema is any schema containing \Delta or \Xi:

\begin{schema}{OperationName}
\Delta State \\        % or \Xi State
input? : Type \\       % inputs (optional)
output! : Type         % outputs (optional)
\where
% predicates
\end{schema}

For each operation, extract:

• Name: The schema name
• Kind: \Delta (state-changing) or \Xi (query)
• State schema: The referenced state schema name
• Inputs: Variables ending in ? with their types
• Outputs: Variables ending in ! with their types
• Predicates: All clauses in the \where block

If --operation=NAME is specified, process only that operation.

3. Resolve Context

Before partitioning, resolve the context each operation needs: