model2code

/z-spec:model2code - Model to Code

Generate implementation code and unit tests from a Z specification.

Usage

/z-spec:model2code [spec.tex] [language]

Arguments:

• spec.tex - Z specification file (default: search in docs/)
• language - Target: swift, typescript, python, kotlin (default: detect from project)

Workflow

Step 1: Validate the Specification

Before generating code, type-check the specification with fuzz:

fuzz -t <spec.tex>

If fuzz reports errors, fix them first. Code generation from invalid specs produces invalid code.

Step 2: Detect Target Language

If no language specified, detect from project files:

File Present	Language
Package.swift, *.xcodeproj	Swift
package.json, tsconfig.json	TypeScript
pyproject.toml, setup.py, requirements.txt	Python
build.gradle.kts, pom.xml	Kotlin

Step 3: Generate Code

Read the Z specification and translate each construct to idiomatic code for the target language.

Translation Principles

State Schemas → Classes/Structs

Z state schemas become data types with properties:

\begin{schema}{Account}
balance : \num \\
status : Status
\where
balance \geq 0 \lor status = suspended
\end{schema}

Swift:

struct Account {
    var balance: Int
    var status: Status

    var isValid: Bool {
        balance >= 0 || status == .suspended
    }
}

TypeScript:

interface Account {
    balance: number;
    status: Status;
}

function isValidAccount(a: Account): boolean {
    return a.balance >= 0 || a.status === Status.Suspended;
}

Free Types → Enums

\begin{zed}
Status ::= pending | active | suspended | closed
\end{zed}

Swift:

enum Status {
    case pending, active, suspended, closed
}

TypeScript:

enum Status {
    Pending = "pending",
    Active = "active",
    Suspended = "suspended",
    Closed = "closed"
}