methodical-programming

Methodical Programming（メソッドによるプログラミング）

厳密で数学的な根拠に基づくプログラム構築と検証の手法を適用します。プログラムは、その場しのぎで記述して後からテストするのではなく、形式仕様から導出します。このスキルは言語に依存せず、あらゆるプログラミングパラダイムに適用できます。

基本原則

1. コードより先に仕様を定める

すべての関数／手続きには、必ず次の仕様を定める必要があります。

• 事前条件（Pre）： 入力が満たす必要のある条件です。
• 事後条件（Post）： 入力と出力の間に成り立つ必要のある関係です。

function f(params) returns results
  {Pre: conditions on params}
  {Post: relations between params and results}

プログラムの実際の動作が仕様と一致するとき、そのプログラムは正しいといえます。事前条件が弱いほど関数の再利用性は高まり、事後条件が強いほど関数は有用になります。

2. 検証より導出を優先する

• 検証： 既存のプログラムが仕様を満たすことを（事後的に）証明します。
• 導出： 仕様から、構成によって正しさが保証されるプログラムを構築します。

常に導出を優先してください。事後条件の分析からコードを導出します。

• プログラム変数と式の間の等式 → 代入によって解きます。
• 事後条件の選言 → 選択肢／条件分岐（if/match/switch）を設計します。
• 事後条件の連言 → 順次合成または条件分岐を試みます。

3. 状態、アサーション、置換

• 状態とは、プログラム内のある時点における、すべての変数とその現在値との対応付けです。
• **アサーション（aserto）**とは、プログラム変数に関する論理式であり、有効な状態の集合を記述します。
• 置換 A[x ← E]：アサーション A 内の x のすべての自由出現を式 E に置き換えます。これは代入を推論するための重要な操作です。

---

命令の意味論（公理的）

言語の構文にかかわらず、次の規則を適用します。

スキップ／何もしない操作

{A} skip {A}

実行前に真であることは、実行後もすべて真です。

代入

{A[x ← E]} x := E {A}

{P} x := E {Q} を証明するには、次を示します。

1. 式 E をエラーなく評価できること。
2. P ⟹ Q[x ← E]（事前条件が、x を E に置き換えた事後条件を含意すること）。

多重代入（同時）

<x₁, x₂, ..., xₙ> := <E₁, E₂, ..., Eₙ>

すべての式は、代入前の値を使って評価されます。右辺の式に変数が含まれる場合は、この点が重要です。

順次合成

{A₁} P₁ ; P₂ {A₃}

中間アサーション A₂ を見つけます。これにより、{A₁} P₁ {A₂} および {A₂} P₂ {A₃} が成り立つようにします。

条件分岐／選択

{Pre}
if B₁ → S₁
   B₂ → S₂
   ...
   Bₙ → Sₙ
end if
{Post}

次を検証します。

1. 網羅性： Pre ⟹ B₁ ∨ B₂ ∨ ... ∨ Bₙ（少なくとも1つの分岐が実行可能であること）。
2. 各分岐の正しさ： 各 i について {Pre ∧ Bᵢ} Sᵢ {Post} が成り立つこと。

関数呼び出し

<x₁, ..., xₘ> := f(e₁, ..., eₖ)

1. 呼び出しの前：引数が関数の事前条件を満たすことを証明します。
2. 呼び出しの後：結果変数が事後条件を満たすことを確認します（パラメーター／結果の名前を置き換えたうえで）。

---

量化子と隠れた操作

仕様を簡潔に表現するには、量化子を使います。それぞれに中立元（空の領域での値）があります。

量化子	記号	中立元	型	説明
総和	Σ	0	数値	領域内の総和
積	Π	1	数値	領域内の積
全称	∀	true	ブール値	領域内の連言（and）
存在	∃	false	ブール値	領域内の選言（or）
カウンター	N	0	自然数	述語が成り立つ箇所の数
最大値	MAX	—	数値	領域内の最大値
最小値	MIN	—	数値	領域内の最小値

量化子の分割 — 領域から要素を1つ取り出し、二項演算で組み合わせます。

Σ(a: 1≤a≤n: f(a)) = Σ(a: 1≤a≤n-1: f(a)) + f(n)
MAX(a: 1≤a≤n: f(a)) = max(MAX(a: 1≤a≤n-1: f(a)), f(n))

中立元は、再帰の基底ケースと反復の初期化値を定義します。

---

代数的データ型

データ型を使用するときは、その代数的仕様を順に考えます。

1. シグネチャ： 型（種）と、引数の数を伴う演算。
2. 等式： 演算の振る舞いを定義する代数的恒等式。
3. コンストラクター： 型の任意の値を構築できる最小限の演算集合（帰納法の基礎として使用します）。

一般的な構造

リスト： コンストラクターは []（空）と e:l（コンス）です。演算は ++（連結）、length です。

[] ++ l₂ ≡ l₂
(e:l₁) ++ l₂ ≡ e:(l₁ ++ l₂)
length([]) ≡ 0
length(e:l) ≡ 1 + length(l)

スタック（LIFO）： コンストラクターは empty_stack と push(e, s) です。演算は top、pop、is_empty です。

top(empty_stack) ≡ error
top(push(e, s)) ≡ e
pop(push(e, s)) ≡ s
is_empty(empty_stack) ≡ true
is_empty(push(e, s)) ≡ false

キュー（FIFO）： コンストラクターは empty_queue と enqueue(e, q) です。演算は front、dequeue、is_empty です。

二分木： コンストラクターは empty_tree と plant(e, left, right) です。演算は root、left、right、is_empty、height、size です。

height(empty_tree) ≡ 0
height(plant(e, a₁, a₂)) ≡ 1 + max(height(a₁), height(a₂))
size(plant(e, a₁, a₂)) ≡ 1 + size(a₁) + size(a₂)

テーブル／マップ： コンストラクターは create と assign(t, index, value) です。演算は lookup、defined です。

コンストラクター集合を使って、各型の帰納構造を特定します。

---

帰納法の原理

データ型の性質を証明するには、コンストラクターを特定し、構造帰納法で考えます。

[P(base) ∧ ∀x (P(smaller(x)) ⟹ P(x))] ⟹ ∀z P(z)

• 基底ケース： 0 項コンストラクターで構築される値（空リスト、空スタックなど）について、性質を証明します。
• 帰納ステップ： すべての部分構造で性質が成り立つと仮定し、それを合成した構造でも成り立つことを証明します。

整礎な前順序（ノエター的順序）が必要です。無限に厳密に減少する列が存在しないことを意味します。これにより、帰納法と再帰が確実に終了します。

---

再帰プログラム

パターン

すべての再帰関数は、次の構造に従います。

function f(x) returns r
  {Pre: Q(x)}
  if d(x) →          // direct case
    r := h(x)
  ¬d(x) →            // recursive case
    v := f(s(x))
    r := c(x, v)
  end if
  {Post: R(x, r)}
  return r

検証手順

1. 直接ケースの正しさ： Q(x) ∧ d(x) ⟹ R(x, h(x))
2. 再帰ケース — 呼び出しの適法性： Q(x) ∧ ¬d(x) ⟹ Q(s(x))（再帰引数で事前条件が成り立ちます）
3. 再帰ケース — 正しさ： Q(x) ∧ ¬d(x) ∧ R(s(x), v) ⟹ R(x, c(x, v))
4. 有界関数 t(x)： 次を満たす t: params → ℕ を定義します。
   • Q(x) ⟹ t(x) ∈ ℕ（常に自然数です）
   • Q(x) ∧ ¬d(x) ⟹ t(s(x)) < t(x)（再帰呼び出しごとに厳密に減少します）

有界関数を選ぶ際のヒント

引数の型	一般的な有界関数
減少する自然数 n	n 自身
一方が常に減少する 2 つの自然数	m + n
一方が減少し、もう一方は増加するが前者に達しない 2 つの自然数	max(m, n)
true → false に変化するブール値 b	if b then 1 else 0
false → true に変化するブール値 b	1 - (if b then 1 else 0)
スタック	height(stack)
キュー	length(queue)
二分木	size(tree) または height(tree)
リスト	length(list)
縮小する区間 [i, j]	j - i

再帰の種類

• 線形再帰： 各呼び出しから生成される再帰呼び出しは最大 1 つです。
• 多重再帰： 1 回の呼び出しから複数の再帰呼び出しが生成される場合があります（例：木の走査）。

再帰プログラムを設計する方法

1. 関数を仕様化します。ヘッダー、事前条件、事後条件を定義します。
2. 有界関数 t(x) を特定します。これは ℕ 上の帰納法に使用する式です。
3. ケースを分析します。少なくとも 1 つの直接ケースと 1 つの再帰ケースを特定します。すべてのケースを網羅してください。
4. 各ケースをプログラムして検証します。再帰ケースでは、帰納法の仮定により、再帰呼び出しが仕様を満たすと仮定します。
5. 停止性を検証します。各再帰呼び出しで t(x) が厳密に減少することを証明します。

---

アルゴリズムへの没入（一般化）

直接的な再帰解法が見つからない場合、効率的でない場合、または推論が難しい場合は、引数や戻り値を追加して関数を一般化します。これは**没入（イマージョン）**と呼ばれます。

手法

前条件の強化

1. 事後条件を弱めます（新しい変数を導入する場合があります）。
2. 弱めた事後条件を使って前条件を強化し、結果の部分版を入力として要求します。
3. 新しい前条件が意味をなすように、イマージョンパラメーターを追加します。
4. 元の事後条件はそのままにします。

弱めた事後条件から、次のアイデアが得られます。

• 基底ケースのガード： 弱めた条件を「反転」させる条件です。
• 再帰ケース： 呼び出し間で変わるのはイマージョンパラメーターだけです → 事後条件が一定の末尾再帰になります。

事後条件を弱める

1. 事後条件の部分式を置き換える新しい変数を導入します。
2. 等式の一部を削除し、要求を弱めます。
3. 削除した等式は、イマージョンから元の関数を復元するための初期化になります。
4. 必要に応じて、新しいパラメーターの定義域条件で前条件を強化します。

効率化イマージョン

複雑な式 f(x) を再帰呼び出しのたびに再計算する必要がある場合：

• 追加の結果として： 事後条件に w = f(x) を追加します。s(x) による再帰呼び出しの後、w を f(s(x)) から f(x) に更新します。
• 追加のパラメーターとして： 前条件に w = f(x) を追加します。f(x) を計算する代わりに w を使います。再帰呼び出しを行う際は、現在の w から新しいパラメーター値を計算します。

展開／畳み込みの手法（末尾再帰への変換）

線形再帰を末尾再帰に変換します。

1. f(x) = c(f(s(x)), x)（線形再帰ケース）が与えられたとき、イマージョン g(y, w) = c(f(y), w) を定義します。
2. 展開： f の各ケースを g の定義に代入します。
3. 畳み込み： 式を変形し、再び g の形に戻します。
4. その結果、末尾再帰の g が得られます。ここで f(x) = g(x, neutral) であり、neutral は c の単位元です。

---

反復プログラム（ループ）

While ループの意味論

{Invariant I}
while B do
  S
end while
{Post: Q}

検証（2 段階）

第 1 段階 — 部分正当性：

1. 反復の開始時に毎回成り立つ条件である不変条件 I を定義します。
2. 初期化： Pre ⟹ I（前条件から不変条件が導かれます）。
3. 維持： {I ∧ B} S {I}（本体の実行後も不変条件が保たれます）。
4. 終了： I ∧ ¬B ⟹ Post（不変条件とループ終了条件から事後条件が導かれます）。

第 2 段階 — 停止性：

1. 値域が ℕ である上界関数 t を定義します。
2. 有界性： I ∧ B ⟹ t > 0。
3. 減少性： {I ∧ B ∧ t = T} S {t < T}（本体によって上界が厳密に減少します）。

変換：末尾再帰 → 反復

事後条件が一定の末尾再帰関数は、直接 while ループに変換できます。

再帰の要素	反復の要素
イマージョンされた関数の前条件	ループの不変条件
上界関数（前順序）	ループの上界関数
イマージョンパラメーター	ループのローカル変数
再帰ケースのガード	ループの条件 B
再帰呼び出しでのパラメーター更新	ループの本体
直接ケースの本体	ループ後のコード
初回呼び出しの引数	ループの初期化（while の前）

反復の直接的な導出

1. 不変条件の中核は通常、弱めた事後条件です。
2. 不変条件を維持し、上界関数を減少させるガード付き命令を設計します。
3. 次の条件を満たすと、必要なケースが網羅されます：Invariant ∧ ¬(B₁ ∨ B₂ ∨ ... ∨ Bₙ) ⟹ Post。

---

ワークフローの概要

関数を書く際は、次のプロセスに従います。

1. 仕様を定める： 事前条件と事後条件を書きます。入力と出力の型を特定します。
2. 事後条件を分析する： 解決策に代入、条件分岐、再帰、反復のどれが必要か判断します。
3. 方針を選ぶ：
   • 等式を含む単純な事後条件 → 直接代入／合成。
   • 選言 → 条件分岐／選択肢。
   • 帰納的な構造 → 再帰または反復。
4. 再帰的な解決策の場合：
   • ケースを特定します（直接ケース＋再帰ケース）。
   • 上界関数を定義します。
   • 各ケースを検証します。
   • 効率化や末尾再帰が必要な場合は、イマージョンを検討します。
5. 反復的な解決策の場合：
   • 不変条件を導出します（弱めた事後条件）。
   • 上界関数を定義します。
   • 不変条件を維持し、上界を減少させるループ本体を設計します。
   • 初期化とループ後のコードを設定します。
6. 検証する： すべての証明義務が満たされていることを確認します。満たされない場合は、構成によってそれらが成り立つコードを導出します。

---

このスキルの適用

あらゆる言語でコードを生成またはレビューする際は、次の点に従います。

• 言語で強制されない場合でも、常に事前条件と事後条件の観点から考えます。コメント、アサーション、型制約、コントラクトとして記述します。
• 言語で利用できるアサーション／コントラクト（assert、require、ensure、デザイン・バイ・コントラクトのライブラリ、プロパティベーステスト）を使って、事前条件と事後条件を表現します。
• 再帰関数を設計するときは、上界関数を明示的に特定し、停止性を検証します。
• ループを設計するときは、不変条件と上界関数を明示的に記述します。
• コードを書いてからテストするのではなく、仕様からコードを導出することを優先します。
• 再帰的な解決策が末尾再帰でない場合は、イマージョン手法による変換を検討します。
• データ構造については代数的な推論を使います。演算を方程式で定義し、構造帰納法で推論します。
• 言語で対応している場合は、上界関数を減少する測度として表現します（例：Dafny の decreases、Coq の構造的再帰、または手動のアサーション）。

---

形式仕様とテストを結び付ける

形式仕様（事前条件と事後条件）とテストは、同じ考えを異なる言語で表現したものです。前者は論理、後者は実行可能なコードで表します。実装ではなく仕様からテストを導出することで、正しいコードを導くのと同じ推論によってテストも正しいものになります。

1. 仕様 → テスト

形式仕様の各要素は、具体的なテストに対応します。

形式的な要素	テストでの対応
事前条件への違反	失敗ケースのテスト — 関数がエラーを通知することを検証します
事後条件の等式 r = E	等式アサーション（toBe、expectEqual、assert { condition = ... }）
事後条件の選言 A ∨ B	分岐ごとに1つのテスト
基底コンストラクター（[]、empty、0）	基底ケースのテスト — 量化子の中立元を検証します
帰納コンストラクター（e:l、plant(...)）	最小の非自明な値を使ったテスト

実例 — sum(list)

function sum(list) returns result
  {Pre:  list is a list of numbers}
  {Post: result = Σ(a: a ∈ list: a)}

Σ の中立元は 0 なので、基底ケースは sum([]) = 0 です。帰納コンストラクター e:l から最小のテスト sum([5]) = 5 が得られ、一般的なケースは sum([1, 2, 3]) = 6 です。

TypeScript（Jest / Vitest）

// sum.test.ts
import { sum } from "./sum";

it("returns 0 for empty list — neutral element of Σ", () => {
  expect(sum([])).toBe(0);
});

it("returns the element itself for a singleton — minimal inductive case", () => {
  expect(sum([5])).toBe(5);
});

it("returns the total for a general list", () => {
  expect(sum([1, 2, 3])).toBe(6);
});

it("rejects non-numbers — precondition violation", () => {
  expect(() => sum(["a"] as any)).toThrow();
});

Go（testing）

// sum_test.go
func TestSumEmptyList(t *testing.T) {
    // Base case: neutral element of Σ is 0
    if got := Sum([]int{}); got != 0 {
        t.Errorf("Sum([]) = %d, want 0", got)
    }
}

func TestSumSingleton(t *testing.T) {
    // Minimal inductive case: one recursive step falling into base case
    if got := Sum([]int{5}); got != 5 {
        t.Errorf("Sum([5]) = %d, want 5", got)
    }
}

func TestSumGeneralList(t *testing.T) {
    if got := Sum([]int{1, 2, 3}); got != 6 {
        t.Errorf("Sum([1,2,3]) = %d, want 6", got)
    }
}

2. 再帰ケースのテスト

すべての再帰関数は、次の構造を持ちます。

function f(x):
  if d(x)  → h(x)           -- direct case
  ¬d(x)    → c(x, f(s(x)))  -- recursive case

この構造から、テストスイートが直接導かれます。

• 直接ケース（d(x) が真）：基本ケースをテストします。期待値は、事後条件が表す量化子の中立元です。
• 最小再帰ケース（¬d(x) で、s(x) が直接ケースに該当する場合）：再帰呼び出しがちょうど1回発生する最小の入力でテストします。
• 一般ケース：再帰呼び出しが複数回発生する入力でテストします。
• 上界関数 t(x)：停止性が自明でない場合は、呼び出しカウンターまたはスパイを使い、再帰呼び出しの回数が t(x_initial) を超えないことを確認します。

例 — length(list)

function length(list) returns n
  {Pre:  list is a list}
  {Post: n = N(a: a ∈ list: true)}
  if list = []  → n := 0                      -- d(x): list is empty
  list ≠ []     → n := 1 + length(tail(list)) -- recursive case

上界関数：t(list) = length(list)（入力構造のサイズ）。

TypeScript（Jest / Vitest）

// length.test.ts
import { length } from "./length";

it("returns 0 for empty list — direct case, neutral of N", () => {
  expect(length([])).toBe(0);
});

it("returns 1 for singleton — one recursive call into base", () => {
  expect(length([7])).toBe(1);
});

it("returns correct length for general list", () => {
  expect(length([1, 2, 3])).toBe(3);
});

Go（testing）

// length_test.go
func TestLengthEmpty(t *testing.T) {
    if got := Length([]int{}); got != 0 {
        t.Errorf("Length([]) = %d, want 0", got)
    }
}

func TestLengthSingleton(t *testing.T) {
    if got := Length([]int{7}); got != 1 {
        t.Errorf("Length([7]) = %d, want 1", got)
    }
}

func TestLengthGeneral(t *testing.T) {
    if got := Length([]int{1, 2, 3}); got != 3 {
        t.Errorf("Length([1,2,3]) = %d, want 3", got)
    }
}

Zig（std.testing + comptime テーブル）

Zig では、複数のケースに対する慣用的なパターンは、comptime 配列に対する inline for です。外部ライブラリを使わず、コストゼロのパラメトリックテストを実行できます。

const std = @import("std");
const length = @import("length").length;

test "length — direct case, recursive case, general" {
    const cases = comptime [_]struct {
        input: []const i32,
        expected: usize,
    }{
        .{ .input = &[_]i32{},        .expected = 0 }, // direct case: d(x)
        .{ .input = &[_]i32{7},       .expected = 1 }, // minimal recursive case
        .{ .input = &[_]i32{ 1, 2, 3 }, .expected = 3 }, // general case
    };

    inline for (cases) |c| {
        try std.testing.expectEqual(c.expected, length(c.input));
    }
}

3. 全称事後条件に対するプロパティベーステスト

事後条件に全称量化子（∀）が含まれる場合、手動テストで検証できるのは、無限にある真のケースのうち有限個だけです。プロパティベーステスト（PBT）はランダムな入力を生成して各入力でプロパティを検証し、失敗時には反例を縮小して、最小の失敗ケースを見つけます。

ルール： 事後条件が ∀x ∈ domain: P(x) の形式であれば、例だけでなくプロパティテストを記述します。

例 — reverse の代数的性質

{Post₁: ∀l: length(reverse(l)) = length(l)}   -- reverse preserves length
{Post₂: ∀l: reverse(reverse(l)) = l}           -- reverse is an involution

TypeScript — fast-check

// reverse.property.test.ts
import * as fc from "fast-check";
import { reverse } from "./reverse";

test("Post₁: reverse preserves length — ∀l", () => {
  fc.assert(
    fc.property(fc.array(fc.integer()), (l) => {
      return reverse(l).length === l.length;
    })
  );
});

test("Post₂: reverse is an involution — ∀l", () => {
  fc.assert(
    fc.property(fc.array(fc.integer()), (l) => {
      const rr = reverse(reverse(l));
      return rr.length === l.length && l.every((v, i) => v === rr[i]);
    })
  );
});

Go — rapid

// reverse_property_test.go
import (
    "testing"
    "pgregory.net/rapid"
)

func TestReversePreservesLength(t *testing.T) {
    // Post₁: ∀l: length(reverse(l)) = length(l)
    rapid.Check(t, func(t *rapid.T) {
        l := rapid.SliceOf(rapid.Int()).Draw(t, "l")
        if len(Reverse(l)) != len(l) {
            t.Fatalf("length(Reverse(%v)) ≠ length(%v)", l, l)
        }
    })
}

func TestReverseIsInvolution(t *testing.T) {
    // Post₂: ∀l: reverse(reverse(l)) = l
    rapid.Check(t, func(t *rapid.T) {
        l := rapid.SliceOf(rapid.Int()).Draw(t, "l")
        got := Reverse(Reverse(l))
        if len(got) != len(l) {
            t.Fatalf("len(Reverse(Reverse(%v))) = %d, want %d", l, len(got), len(l))
        }
        for i := range l {
            if got[i] != l[i] {
                t.Fatalf("Reverse(Reverse(%v)) = %v, want %v", l, got, l)
            }
        }
    })
}

Zig — comptime テーブル + 組み込みファザー

Zig には、慣用的な PBT ライブラリはありません。次の2つの方法を組み合わせて使います。

1. 仕様から導いた代表的なケース（基本ケース、最小帰納ケース、境界値）に対して、comptime 配列で inline for を使います。
2. クラッシュやパニックが発生しないことの不変条件には、zig test --fuzz を使います。組み込みファザーが任意のバイト列を入力し、パニック、範囲外アクセス、未定義動作を検出します。

const std = @import("std");
const reverse = @import("reverse").reverse;

// Post₁ + Post₂: representative cases covering base and inductive constructors
test "reverse — spec-derived cases" {
    const allocator = std.testing.allocator;
    const cases = comptime [_]struct {
        input: []const i32,
        expected: []const i32,
    }{
        .{ .input = &[_]i32{},        .expected = &[_]i32{} },
        .{ .input = &[_]i32{1},       .expected = &[_]i32{1} },
        .{ .input = &[_]i32{ 1, 2, 3 }, .expected = &[_]i32{ 3, 2, 1 } },
    };

    inline for (cases) |c| {
        const result = try reverse(allocator, c.input);
        defer allocator.free(result);
        try std.testing.expectEqual(c.expected.len, result.len);
        try std.testing.expectEqualSlices(i32, c.expected, result);
    }
}

// Post₁ no-panic invariant: reverse must not crash on any input
test "reverse — fuzz no-panic" {
    const input = std.testing.fuzzInput(.{});
    const allocator = std.testing.allocator;
    const n = input.len / @sizeOf(i32);

    // Decode fuzz bytes into i32 values without assuming alignment.
    var buf = std.ArrayList(i32).init(allocator);
    defer buf.deinit();
    try buf.ensureTotalCapacity(n);

    var i: usize = 0;
    while (i < n) : (i += 1) {
        const base = i * @sizeOf(i32);
        const chunk = input[base .. base + @sizeOf(i32)];
        const value = std.mem.bytesToValue(i32, chunk);
        buf.appendAssumeCapacity(value);
    }

    const data: []const i32 = buf.items;
    const result = reverse(allocator, data) catch return;
    defer allocator.free(result);
    try std.testing.expectEqual(data.len, result.len);
}
// Run with: zig test reverse_test.zig --fuzz

Terraform — ネイティブの terraform test（.tftest.hcl）

Terraform には PBT がありません。全称事後条件（∀）は、assert ブロック内で alltrue([for ... : ...]) を使って表現します。境界ケースと事前条件違反には、それぞれ個別の run ブロックを用意します。.tftest.hcl ではループを使えません。

# tests/subnets_unit_test.tftest.hcl

# Post: ∀subnet ∈ aws_subnet.private: subnet.cidr_block ∈ "10.0.0.0/8"
run "all_private_subnets_in_range" {
  command = plan

  assert {
    condition = alltrue([
      for s in aws_subnet.private : can(regex("^10\\.0\\.", s.cidr_block))
    ])
    error_message = "All private subnets must be in the 10.0.x.x range."
  }
}

# Pre violated: cidr_block outside allowed range must be rejected
run "invalid_cidr_rejected" {
  command = plan

  variables {
    cidr_block = "192.168.1.0/24"
  }

  expect_failures = [var.cidr_block]
}

# Boundary: minimum allowed subnet count
run "minimum_subnet_count" {
  command = plan
  variables { subnet_count = 1 }

  assert {
    condition     = length(aws_subnet.private) == 1
    error_message = "Expected exactly 1 subnet."
  }
}

# Boundary: zero subnets must be rejected by variable validation
run "zero_subnets_rejected" {
  command = plan
  variables { subnet_count = 0 }

  expect_failures = [var.subnet_count]
}

4. 組み合わせたワークフロー

形式的な導出と TDD は、どちらかを選ぶものではありません。同じプロセスを構成する2つの層です。仕様を信頼できる唯一の情報源とし、コードとテストは、それぞれ独立に仕様から導出します。

1. Specify   Write Pre and Post formally.
             Identify the quantifier structure (Σ, ∀, N, ...) and its neutral element.
             Identify constructors of the input type (base + inductive).

2. Red       Translate Pre/Post into tests — all must fail (code does not exist yet):
             · Pre violated              → unhappy-path test / expect_failures
             · Base constructor          → test of the quantifier's neutral element
             · Minimal inductive case    → test with one recursive step into base
             · Postcondition with ∀      → property test (fast-check / rapid)
                                           or alltrue([for...]) in Terraform
             · Each postcondition branch → one test per disjunct

3. Derive    Construct the code from the postcondition analysis (not from the tests).
             Choose the strategy that matches the postcondition structure:
             equalities → assignment, disjunctions → conditional, inductive → recursion/loop.

4. Green     The tests pass on the first run — by construction, not by adjustment.
             If a test fails, the derivation has a gap: re-examine the proof obligation.

5. Refactor  Improve structure, names, efficiency. The tests stay green.
             The formal invariant guarantees that refactoring preserves correctness.
             Immersion (tail-recursion transformation) is a safe refactoring step
             because the postcondition is unchanged.

重要なポイント： コードとテストの両方を同じ仕様から導出すると、レッド・グリーン・リファクタリングのサイクルは、仕様化 → 導出 → 検証に集約されます。実装ではなく仕様に基づいて記述されたテストは、テストにたまたま合致する誤ったコードによって、誤って合格することはありません。正しい理由で失敗し、正しい理由で合格します。