Generate TypeScript/Python code scaffolds from VDM-SL specifications. Triggered by "generate code from the spec", "convert to TypeScript", "generate Python code", "create a scaffold", "generate implementation template", "create type definitions from VDM", or "generate agent code". Also responds to Japanese: 「仕様からコードを生成して」「TypeScriptに変換して」等。 Generates runtime verification code for pre-conditions, post-conditions, and invariants.
How this skill is triggered — by the user, by Claude, or both
Slash command
/formal-agent-contracts:generate-codeThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
Read VDM-SL specifications (types, functions, operations, invariants) and generate
Read VDM-SL specifications (types, functions, operations, invariants) and generate TypeScript or Python implementation scaffolds. Includes runtime verification (pre/post/inv checks).
VDM-SL仕様を読み取り、TypeScript/Pythonの実装スキャフォールドを生成する。 ランタイム検証(pre/post/inv チェック)も含める。
Read the .vdmsl file specified by the user.
If no file is specified, search for .vdmsl files in the workspace.
ユーザーが指定した .vdmsl ファイルを読み取る。指定がなければワークスペース内を探索。
If the user hasn't specified, ask with AskUserQuestion:
ユーザーが明示しない場合、AskUserQuestionで確認する。
Follow the conversion rules in references/typescript-rules.md or references/python-rules.md.
references/typescript-rules.md または references/python-rules.md の変換ルールに従う。
Generated file structure:
TypeScript:
generated/
├── types.ts -- Type definitions (interface/type)
├── contracts.ts -- Pre/post/invariant verification functions
├── <module>.ts -- Function/operation implementation scaffolds
└── index.ts -- Exports
Python:
generated/
├── types.py -- Type definitions (dataclass)
├── contracts.py -- Pre/post/invariant verification functions
├── <module>.py -- Function/operation implementation scaffolds
└── __init__.py -- Exports
Convert VDM-SL types to target language types. See references for detailed rules.
VDM-SL型をターゲット言語の型に変換する。変換ルールの詳細はリファレンス参照。
Core mapping:
| VDM-SL | TypeScript | Python |
|---|---|---|
nat, nat1, int | number | int |
real | number | float |
bool | boolean | bool |
seq of char | string | str |
seq of T | T[] | list[T] |
set of T | Set<T> | set[T] |
map K to V | Map<K, V> | dict[K, V] |
| Record type | interface | @dataclass |
[T] (option) | T | null | Optional[T] |
| Union type | union type | Union[...] |
Generate runtime check functions for invariants, pre-conditions, and post-conditions.
不変条件・事前条件・事後条件をランタイムチェック関数として生成する。
Policy:
VDM_CONTRACT_CHECKExplicit definitions → convert implementation where possible
Implicit definitions (pre/post only) → generate stubs with TODO comments
明示的定義 → 可能な範囲で実装を変換。暗黙的定義 → TODO付きスタブを生成。
// VDM-SL: findUser(uid, users) == users(uid) pre uid in set dom users
function findUser(uid: UserId, users: Map<UserId, User>): User {
// Pre-condition check
assert(users.has(uid), `Pre-condition failed: uid ${uid} not in users`);
// Implementation
const result = users.get(uid)!;
return result;
}
Place generated code in a generated/ subfolder in the same directory as the spec file.
If files already exist, ask the user for overwrite confirmation.
生成したコードを仕様ファイルと同じディレクトリの generated/ に配置する。
TODO comments生成コードはそのまま動作可能な状態を目指す。TODOで手動実装箇所を明示。
JSDoc/docstringで元のVDM-SL定義を記載。エラーメッセージは具体的に。
The following constructs cannot be generated and should be noted with TODO comments:
以下はコード生成を断念し TODO コメントで注記する:
exists / exists1 quantifiers → describe semantics in comments{k |-> v | ...} → convert to loop construction or TODOreferences/typescript-rules.md — Complete TypeScript conversion rulesreferences/python-rules.md — Complete Python conversion rulesnpx claudepluginhub kotaroyamame/formal-agent-contracts --plugin formal-agent-contractsGuides Python type hints, mypy static checking with configs, modern syntax, and advanced features like Protocol, TypedDict, Generics for type-safe code.
Generates backend service implementations with business logic from OpenAPI specs, data models, and scaffold stubs. Use when implementing service layers from TODO stubs.
Guides creation, editing, and verification of skills for AI coding agents using test-driven development with subagent scenarios. Use when authoring or debugging skills.