spec-template

要件定義をコードに落とすための足場。 不変条件を一次成果物として扱い、 主張と強制機構と検査を機械的に照合し続けるための仕組み一式です。

最初にやること

npm install
npm test        # 緑。機構が動くところを見る
npm run spec    # 緑。モデル検査（安全性 / 活性 / 介入の列挙）
npm run check   # ⚠️ 赤で始まります（意図的）

npm run check は例が残っているあいだ赤です。（npm run template:replaced が落とす） コミットは通ります — フックが走らせるのは check:quick までなので、 置き換えの途中でも作業を記録できます。

照合はどれも相対的で「互いに一致しているか」しか見ません。だから機構だけコピーして 中身を書かないと、緑になる空の網ができあがり、しかも本物と見分けがつきません。 それを防ぐために、src/domain/example/ が存在するあいだは落ちるようにしてあります。

置き換える順序

1. docs/design/questions.md を使って要件を聞く
2. docs/design/context.md の確定 / 却下 / 未決 を埋める
3. src/invariants/registry.ts と assumptions.ts の例を消し、自分のものを書く
4. src/domain/example/ を消し、自分のドメインを書く
5. spec/lifecycle.qnt の例を消し、自分のモデルを書く

未決事項が残っている領域の状態遷移コードは書かないこと。

何が何を担保しているか

docs/design/pipeline.md を読んでください。要件がコードになるまでに何段あり、 各段で何が落ち、何がそれを捕まえるかの地図です。

前提 — Java が要るのは verify だけ

Quint 自体は TypeScript ですが、quint verify は検査を Apalache（Scala）と TLC（Java）に投げます。--backend=tlc でも Quint → TLA+ の翻訳を Apalache が 担うため、どちらの backend でも JDK 17 以上が要ります。

コマンド	Java
npm run spec:typecheck / quint run / quint test	不要
npm run spec / spec:mutation	必要

反例を探す作業は Java 無しででき、「反例が無い」と言うときだけ JVM が要ります。 quint run はランダムに撒いているだけなので、反例が出ないことに意味はありません。 無いと言えるのは verify だけです。

Java が見つからない場合は scripts/verify-spec.sh が読めるエラーで止まります （JVM の起動失敗をそのまま見せない）。