kaedeasset記事 · Notes霧走町 流氷に眠る

台本を一度も流さずに、47 の規則で作品データを検査する

Checking the game data with 47 rules without running the script once

 D17-4-T34-lint-static-analysis・技術・日本語入力でプレイする仕組み

確かめ方static analysislintinvariant checkingdata-flow analysis (fixed point)claude自然言語処理

『霧走町 流氷に眠る』の作品データは、ゲームを 1 手も動かさずに、47 の規則で検査しています。
フラグの宣言漏れから、「まだ明かしていない名前を、台詞が先に口にしていないか」まで。今日の全三章のデータで 0.99 秒、エラー 0・警告 1 でした。2026-10-29 に測った値です。

今日から、確かめ方の回に入ります(T34〜T49)。
最初は、実行せずに見る検査です。明日の T35 は、同じく実行せずにクリアまでの手を逆算する道具、その夜の T36 は逆に、状態を全部歩いて確かめる道具です。

この回の位置と、前後の回#

区切り: T34〜T49 確かめ方(16 回のうち 1 回目)
先に読むとよい回: T01(全体の構造と、使っている技術と言語)
次に読む回: T35(解ける道を逆算する)

名前 — static analysis#

正式名
static analysis(静的解析)/lint
近い名前
invariant checking(不変条件の検査)・data-flow analysis(データフロー解析)の fixed point(不動点)の計算

初出:
static analysis という語の初出は確かめられませんでした。
lint の名前は、Stephen C. Johnson の "Lint, a C Program Checker"(Bell Laboratories, Computing Science Technical Report 65)から来ています。日付は資料で割れていて、1977 年 12 月とするものと、1978 年とするものがあります。
不動点で流れを解く枠組みの古典は Kildall "A unified approach to global program optimization"(POPL 1973)、それを近似の理論としてまとめたのが Cousot & Cousot "Abstract interpretation"(POPL 1977)です。

一般の解説 — static analysis#

静的解析は、プログラムを実行せずに、書かれた物だけを見て性質を調べることです。
コンパイラの型検査も、lint も、データフロー解析も、その仲間です。

Johnson の lint は、C のコンパイラが見逃す「たぶん誤り」と「移植できない書き方」を、ソースだけから拾う道具でした。型の規則をコンパイラより厳しく当て、複数のファイルにまたがる関数の呼び方の食い違いも見ました。
今では、言語ごとの規則の束を当てる道具を広く lint と呼びます。

もう少し深い解析は、プログラムの流れの上で「各地点で何が成り立ちうるか」を集合として持ち、変わらなくなるまで繰り返し広げます(不動点の計算)。
集合が単調にしか増えず、有限なら、必ず止まります。

よく知られた性質が二つあります。

一つ目、健全さ(soundness)と完全さ(completeness)は両立しない。プログラムの意味に関わる性質は、一般には実行せずに決められない(Rice の定理)ので、解析は「起きうるかもしれない」を多めに言う(誤検知)か、「起きる」を見逃す(見逃し)か、どちらかに寄せます。
二つ目、誤検知が多いと人が警告を読まなくなる。規則を足すほど、黙らせる例外も増えます。

うちの lint#

コマンドは adv-sim lint --data Game/adv の 1 本です。
見る物は C++ ではなく、作品データ(意図・段・台本・場所・在席・フラグの宣言・手帳・ヒント・固有名詞の辞書)です。
作りの方針は、作品のデータの不変条件を「コードで禁止せず、検査で落とす」です。読み込みでは弾かず、lint がエラーとして名前を挙げます。

今日の出力の末尾です。

L39(warn): entity hal の別名「ハル」は仮名2文字(ふつうの文に紛れて名指しになる)
…
L48: 手帳のヒント 46 件・対応先の無いもの 0 件
lint: 0 error(s), 1 warning(s) — locations=10 intents=248 flags=102 entities=61

規則の番号は L1〜L48 で、L11 は欠番。47 種です。実装は adv-sim の main.cpp の 1 つの関数で、756 行目から 4781 行目まで、約 4,000 行あります。
番号ごとの意味は、6 つの群に分けると見通せます。

① 参照の整合。宣言していないフラグを要る・立てる(L1)、id の重複(L1)、台本の参照先のファイルと鍵が無い(L5)、固有名詞の辞書に無い id を材料にしている・別名が 2 つの語に重なっている(L6)、人物のプロフィールが無い話者(L8)。
② 形の不変条件。どの意図にも、前提なしの段 0 がある(L3)。言い換えが下限より少ない(L7。本筋は 10 本、雑談は 6 本)。雑談は進行に触れない(L15)。疑いの段はフラグを立てない(L21)。
③ 到達性。宣言したフラグの全部に、立てる道がある(L2)。
④ 名前の先出し。辞書で「このフラグが立つまで明かさない」と宣言した名前を、そのフラグの前に台詞・手帳の文・言い直しが口にしていない(L26)。
⑤ 検査の文の写し込み。凍結した検査の入力が、言い換えの辞書に写っていない(L4・L18・L37。Jaccard 係数で見る。T43 で書きます)。
⑥ 量の報告。話者ごとの台詞の行数と字数(L43)、クリア経路で人物が何手目に初めて出るか(L40)、手帳のヒントの数と対応先(L48)。

② の例: 雑談は進行に触れない#

雑談の意図(町の天気や朝食の時間の話)は、事件のクリア経路を変えないための入れ物です。フラグも手帳も持てません。
L15 はそれを、こう書いています(写す)。

for (const kaede::adv::Intent& It : Intents.intents)
{
	if (!It.bSmalltalk) { continue; }
	…
	for (size_t i = 0; i < It.stages.size(); ++i)
	{
		const kaede::adv::IntentStage& St = It.stages[i];
		if (!St.sets.empty())
		{
			std::printf("L15: %s#%zu: 雑談がフラグを立てている(進行に影響してしまう): %s\n",
				It.id.c_str(), i, St.sets[0].c_str());
			++Errors;
		}
		if (!St.note.empty()) { … "雑談が手帳に書いている(事件の記録ではない)" … }
	}
}

ここが緩むと、書き足した雑談が静かに進行を変えます。照合の点数がどうであれ、雑談に当たった入力で捜査が進むことは、データの形の上で起きない。T01 で書いた「言っていないことで捜査が勝手に進む事故を、精度ではなく構造で止める」を、検査の側から支えている規則です。

③ の例: フラグの到達性は不動点で#

L2 は、初期のフラグから始めて、「前提を満たした段が立てるフラグ」「入れる場所が入ったときに立てるフラグ」「場所の出来事が立てるフラグ」を、増えなくなるまで足し続けます(写す)。

std::set<std::string> Reach(Engine.data.initial.flags.begin(), Engine.data.initial.flags.end());
bool bChanged = true;
while (bChanged)
{
	bChanged = false;
	for (const kaede::adv::Location& L : Engine.data.locations)
	{
		if (!kaede::adv::AdvState::met(L.requiresFlags, Reach)) { continue; }
		for (const std::string& S : L.enterSets) { if (Reach.insert(S).second) { bChanged = true; } }
		…(場所の出来事も同じ)
	}
	for (const kaede::adv::Intent& It : Intents.intents)
		for (const kaede::adv::IntentStage& St : It.stages)
			if (kaede::adv::AdvState::met(St.requiresFlags, Reach))
				for (const std::string& S : St.sets) { if (Reach.insert(S).second) { bChanged = true; } }
}
for (const std::string& F : Declared)
	if (Reach.count(F) == 0 && Engine.data.manualFlags.count(F) == 0)
		std::printf("L2: flag unreachable: %s\n", F.c_str());

この作品のフラグは、立てたら下ろしません。なので集合は単調に増えるだけで、フラグの数(102)を超えて回ることはなく、必ず止まります。一般の解説の不動点の計算の、いちばん素直な形です。

④ の例: 明かしていない名前#

固有名詞の辞書(entities.json)で、名前ごとに「このフラグが立つまで世界は口にしない」と宣言できます。
L26 は、台本の文・手帳に書く文・言い直しの文を正規化して、その名前の別名のどれかを含むかを探します。含んでいたら、その段が「そのフラグを前提に持つ」か「そのフラグを立てる段そのもの」かを見ます。

auto Gated = [&](const std::vector<std::string>& A, const std::vector<std::string>& B,
                 const std::vector<std::string>& Sets, const std::string& Flag)
{
	if (Always.count(Flag)) { return true; }
	for (const std::string& S : Sets) { if (S == Flag) { return true; } } // ここが明かす場面
	for (const std::string& R : A) { if (R == Flag) { return true; } }
	for (const std::string& R : B) { if (R == Flag) { return true; } }
	return false;
};

どちらでもなければ「その名を、そのフラグの成立前に世界が口にしている」でエラーです。
この規則ができる前に一度、まだ名前を知らないはずの場面で、主人公の台詞が名前を口にしていました。原因は、二つの違う「知ったこと」を一つのフラグに相乗りさせていたことでした。以来、フラグは「何を知ったか」の単位で分けています。

⑥ の例: 数えて出すだけの行#

lint には、合否に入らず、量を数えて出すだけの行もあります。今日の L43 から、第一章の人物と主人公だけを写します(全三章ぶんの量です。第二章以降の人物の行は伏せます)。

L43: 堂本  台詞 431 行 / 12557 字
L43: ハル  台詞 148 行 /  4152 字
L43: 佐伯  台詞 151 行 /  3587 字
L43: 源三  台詞 112 行 /  3092 字
L43: 岬    台詞 125 行 /  3077 字
L43: 主人公「刑事」 台詞 469 行 / 9623 字
全体: 話者 9 人 / 台詞 43328 字 / 地の文 26159 字 / 合計 69487 字

主人公の行は、作品の設定で宣言した呼び名で数えます。端役の声(「職員」「女の声」)が台本にしか出ない話者に混じるので、件数だけでは「主人公が台本で一言も喋っていない」を見つけられなかったからです(別の作品で、実際にそうなっていました)。
L40 は、クリアまでの順路(T35 の逆算と同じ計算)で、人物が何手目に初めて出るかです。今日は堂本が 1 手目、佐伯が 7 手目、ハルが 10 手目でした。

規則はどこから来たか#

47 の規則の多くは、机の上で考えたものではありません。
人や AI に遊ばせて引っかかった所を、直すだけでなく規則にして、二度と遊ばせて見つける必要が無いようにしたものです。焦点の文の語で聞いても弾かれる罠(L24)、救済の助言が実際に届くか(L27)、地の文が人物の台詞になっている(L31)などがそうです。

名前どおりでない所 — static analysis#

static analysis / lint と呼ぶのは、名前どおりです(名前の対照表でも ◎ にしています)。実行せずに、書かれた物の規則を当てています。
違う所は三つです。

一つ目、見ているのはプログラムではなくデータです。データの不変条件を当てているので、invariant checking と呼ぶ方が近い規則も多くあります。
二つ目、健全ではありません。L2 は段の前提だけを見て、意図そのものの前提と、その人がその場所にいるか(在席)を見ていません。なので「立てる道がある」と言っても、実際に歩ける道とは限りません(見逃し側に寄っています)。歩ける道かは、在席まで辿る T35 の逆算と、状態を全部歩く T36 で見ます。
三つ目、L26 は逆に、誤検知側に寄っています。「前提に名指しで書いてあるか」しか見ないので、別のフラグから必ずそのフラグが立っている場合でも、エラーにします。そういう場合は前提を書き足して黙らせます。

⑥ の量の報告は、検査ではなく計測です。合否に入れていません。

弱点と、採らなかった案 — static analysis#

  • 規則が 1 つの関数に 4,000 行あります。規則を足すたびに長くなり、どの番号がどこにあるかは文字列を探して見つけています
  • 1 つの番号に複数の検査が入っている所があります(L15 は confirmText・フラグ・手帳の 3 つ、L21 も 3 つ)。番号で数えると 47 ですが、検査の数はそれより多い
  • 文書の規則の表が古くなっています。設計の文書(arch §10.2)の表は L37 で止まり、回帰テストの見出しは「L1-L38」のままでした。今日数えたソースが正です
  • 警告は終了コードを変えません。L39 の警告(「ハル」は仮名 2 文字で、ふつうの文に紛れて名指しになりうる)は、分かったうえで残しています。ハルの名前を変えるより、照合の側で扱う方を選んだからです
  • 名前の先出しを語の形まで見る版は、静的には採りませんでした。同じ日に実装して測ると、静的には 18 件が「起きうる」で赤になり、黙らせるのにフラグの含意の不動点と例外の規則が二つ要りました。実際のプレイを見る側(実フラグと実入力を持っている)に置いています

採らなかった案:

  • 読み込みのときに弾く(エラーで起動しない)。それだと、作者が lint を回す前に、ゲームを立てたときに初めて分かる形になりうる。lint は作者の手元と回帰テストで落とす
  • JSON Schema だけで書く。形の検査はできても、ファイルをまたぐ規則(宣言とフラグの参照・不動点・名前と前提)は書けない

検索語#

static analysis soundness completeness
lint C program checker Johnson
data-flow analysis fixed point Kildall
abstract interpretation Cousot

全三章の製品版は 2027年 発売予定で、Steam でウィッシュリストに入れられます。プロフィールのリンクから。

#claude #自然言語処理