# 画面設計書 40-DrNimメイン画面

## 概要

本ドキュメントは、Nimコンパイラプロジェクトの静的検証ツール「DrNim」のメイン画面の画面設計書である。DrNimはZ3ソルバーを使用した形式検証ツールで、Nimコードの正当性を数学的に証明する。

### 本画面の処理概要

DrNimは、Z3定理証明器を活用してNimコードの形式検証を行うツールである。関数の事前条件（requires）・事後条件（ensures）・不変条件（invariant）などの契約プログラミング記述を検証し、プログラムの正当性を静的に証明する。

**業務上の目的・背景**：プログラムの正当性を実行時ではなくコンパイル時に証明することで、バグの早期発見とソフトウェアの信頼性向上を実現する。特に配列境界チェック、数値範囲検証、不変条件の保証などを自動的に行う。「Doctor Nim」の名前は、プログラムを「診断」して問題を見つけるという意味を込めている。

**画面へのアクセス方法**：コマンドラインから`drnim [options] <projectfile>`の形式で実行する。Z3ライブラリが必要（Unix環境では静的リンク、Windowsでは動的リンク）。

**主要な操作・処理内容**：
1. コマンドライン引数を解析
2. プロジェクトファイルを読み込み
3. セマンティック解析パスを実行
4. strongSemCheck()で各関数の検証を実行
5. Z3ソルバーで条件の充足可能性を判定
6. 検証結果（成功/警告）を出力

**画面遷移**：
- 遷移元：コマンドラインまたはビルドスクリプト
- 遷移先：なし（検証結果出力後に終了）

**権限による表示制御**：特になし。CLIツールとして実行権限があれば使用可能。

## 関連機能

| 機能No | 機能名 | 関連種別 | 関連する操作・処理 |
|--------|--------|----------|------------------|
| 28 | DrNim | 主機能 | Z3ソルバーを使用した静的検証のメイン処理 |
| 4 | セマンティック解析 | 補助機能 | 形式検証のためのセマンティック解析 |

## 画面種別

CLIコマンド実行画面（静的形式検証）

## URL/ルーティング

```
drnim [options] <projectfile>
```

## 入出力項目

### 入力項目

| 項目名 | 型 | 必須 | 説明 | 例 |
|--------|-----|------|------|-----|
| projectfile | path | Yes | 検証対象のNimファイル | main.nim |
| --assumeUnique | flag | No | refポインタの一意性を仮定 | なし |
| その他オプション | - | No | Nimコンパイラと同じオプション | -d:debug |

### 契約プログラミング記法

| プラグマ | 説明 | 例 |
|----------|------|-----|
| requires | 関数の事前条件 | {.requires: x > 0.} |
| ensures | 関数の事後条件 | {.ensures: result > 0.} |
| invariant | ループ不変条件 | {.invariant: i >= 0.} |
| assume | 仮定として追加 | {.assume: len(a) > 0.} |
| assert | 証明対象の表明 | {.assert: x + y > 0.} |

### 出力項目

| 項目名 | 型 | 説明 |
|--------|-----|------|
| 検証結果 | stdout | 成功メッセージまたは警告 |
| 警告メッセージ | stderr | 証明できなかった条件 |
| 反例 | stderr | Z3が生成した反例（存在する場合） |

## 表示項目

| 項目 | 表示形式 | 説明 |
|------|----------|------|
| 警告 | "cannot prove: {condition}" | 条件を証明できない場合 |
| 反例 | "; counter example: {values}" | 証明失敗時の具体例 |
| 成功 | 標準の成功メッセージ | エラーなしで完了時 |

## イベント仕様

### 1-DrNim起動処理

DrNimが起動されると以下の処理が行われる：

1. handleCmdLine()でコマンドライン処理開始
2. optStaticBoundsCheckオプションを有効化
3. processCmdLine()でオプション解析
4. --assumeUniqueオプションがあればフラグ設定
5. newModuleGraph()でモジュールグラフ生成
6. mainCommand()を呼び出し

### 2-メインコマンド実行

mainCommand()では以下の処理を実行：

1. strongSemCheck関数を登録（1197行目）
2. compatibleProps関数を登録（1198行目）
3. "nimcheck"と"nimDrNim"シンボルを定義
4. verbosePassとsemPassを登録
5. compileProject()でプロジェクトをコンパイル
6. エラーがなければ成功メッセージ出力

### 3-強力なセマンティックチェック

strongSemCheck()（1176行目）で各関数を検証：

1. DrnimContextを生成
2. setupZ3()でZ3コンテキストを初期化
3. traverse()でAST全体を走査
4. 各ノードタイプに応じた検証処理
5. ensuresCheck()で関数の事後条件を検証
6. Z3_del_context()でクリーンアップ

### 4-証明エンジン

proofEngine()およびproofEngineAux()で証明を実行：

1. 事実（facts）をZ3の論理式に変換
2. 証明対象をZ3の論理式に変換
3. 否定を取ってZ3ソルバーに投入
4. Z3_solver_check()で充足可能性判定
5. Z3_L_FALSEなら証明成功
6. そうでなければ反例を生成

## データベース更新仕様

本ツールはファイルシステム操作のみを行い、データベースは使用しない。

| 操作（イベント） | 対象 | 操作種別 | 概要 |
|----------------|------|---------|------|
| なし | - | - | データベース操作なし |

## メッセージ仕様

| メッセージID | 種別 | メッセージ内容 | 表示条件 |
|-------------|------|---------------|----------|
| MSG001 | 警告 | "cannot prove: {条件}" | 条件を証明できない |
| MSG002 | 警告 | "; counter example: {反例}" | 反例が存在する場合 |
| MSG003 | エラー | "; cannot map to Z3: {式}" | Z3に変換できない式 |
| MSG004 | 情報 | バージョン情報 | ヘルプ表示時 |

## 例外処理

| 例外条件 | 処理内容 | エラーメッセージ |
|----------|----------|-----------------|
| Z3変換不可 | CannotMapToZ3Errorをスロー | "cannot map to Z3: {式}" |
| Z3エラー | Z3Exceptionをスロー | Z3のエラーメッセージ |
| 引数不足 | ヘルプを表示して終了 | ヘルプメッセージ |

## 備考

- Z3はMicrosoft Researchが開発したSMT（Satisfiability Modulo Theories）ソルバー
- Unix環境ではdist/z3/build/libz3.aを静的リンク
- --assumeUniqueオプションは解析を非健全にするが、Nimコンパイラ自体の検証などに有用
- 整数、浮動小数点、ブール型をZ3の対応する型にマッピング
- 配列アクセスの境界チェックはoptStaticBoundsCheckで有効化
- forall/existsなどの量化子もサポート
- 「old」演算子で関数呼び出し前の値を参照可能

---

## コードリーディングガイド

本画面を理解するために参照すべきファイルと、推奨する読み解き順序を以下に示す。

### 推奨読解順序

#### Step 1: メイン処理フローを理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 1-1 | drnim.nim | `drnim/drnim.nim` | handleCmdLine()（1246-1261行目）、mainCommand()（1193-1208行目） |

**主要処理フロー**:
- **1247行目**: optStaticBoundsCheckを有効化
- **1257行目**: processCmdLineAndProjectPath()でコマンドライン処理
- **1260行目**: mainCommand()呼び出し
- **1197行目**: strongSemCheck関数の登録

#### Step 2: コンテキストとデータ構造を理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 2-1 | drnim.nim | `drnim/drnim.nim` | DrnimContext型（68-81行目）、DrCon型（82-88行目） |

**主要データ構造**:
- **z3**: Z3_context - Z3ソルバーのコンテキスト
- **facts**: seq[(PNode, VersionScope)] - 既知の事実リスト
- **varVersions**: seq[int] - SSA形式の変数バージョン管理
- **mapping**: Table[string, Z3_ast] - Nim式からZ3式へのマッピング

#### Step 3: 検証エンジンを理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 3-1 | drnim.nim | `drnim/drnim.nim` | proofEngineAux()（618-676行目） |
| 3-2 | drnim.nim | `drnim/drnim.nim` | nodeToZ3()（351-525行目） |

**主要処理フロー**:
- **643行目**: Z3ソルバー生成
- **645-651行目**: 事実をZ3式に変換
- **653行目**: 証明対象をZ3式に変換
- **659行目**: 否定を取って検証
- **667行目**: Z3_solver_check()で判定

#### Step 4: AST走査と検証を理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 4-1 | drnim.nim | `drnim/drnim.nim` | traverse()（1045-1174行目） |
| 4-2 | drnim.nim | `drnim/drnim.nim` | strongSemCheck()（1176-1190行目） |

**主要処理フロー**:
- **1057-1063行目**: 関数呼び出し時のrequires/ensures検証
- **1088-1089行目**: try文とpragma文の処理
- **1168-1172行目**: 配列アクセスの境界チェック

### プログラム呼び出し階層図

```
main() [1267-1272行目]
    │
    └─ handleCmdLine()
            │
            ├─ processCmdLine() / オプション解析
            │       │
            │       └─ processSwitch() / 各オプション処理
            │
            ├─ newModuleGraph()
            │
            └─ mainCommand()
                    │
                    ├─ registerPass(verbosePass)
                    │
                    ├─ registerPass(semPass)
                    │       │
                    │       └─ strongSemCheck() [コールバック]
                    │               │
                    │               ├─ setupZ3() / Z3初期化
                    │               │
                    │               ├─ traverse() / AST走査
                    │               │       │
                    │               │       ├─ requiresCheck() / 事前条件
                    │               │       │
                    │               │       ├─ collectEnsuredFacts()
                    │               │       │
                    │               │       ├─ checkBounds() / 境界チェック
                    │               │       │
                    │               │       └─ prove() / 証明実行
                    │               │               │
                    │               │               └─ proofEngine()
                    │               │                       │
                    │               │                       └─ proofEngineAux()
                    │               │                               │
                    │               │                               ├─ nodeToZ3() / Z3変換
                    │               │                               │
                    │               │                               └─ Z3_solver_check()
                    │               │
                    │               └─ ensuresCheck() / 事後条件
                    │
                    └─ compileProject()
```

### データフロー図

```
入力ファイル (.nim)
        │
        ▼
┌─────────────────┐
│  セマンティック解析  │
│   (semPass)     │
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│ strongSemCheck  │
│  AST走査開始     │
└────────┬────────┘
         │
    ┌────┴────┐
    │         │
    ▼         ▼
┌───────┐ ┌───────┐
│ facts │ │証明対象│
│ 収集  │ │ 抽出  │
└───┬───┘ └───┬───┘
    │         │
    ▼         ▼
┌─────────────────┐
│   nodeToZ3()    │
│  Nim→Z3変換     │
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│    Z3 Solver    │
│ 充足可能性判定   │
└────────┬────────┘
         │
    ┌────┴────┐
    │         │
    ▼         ▼
┌───────┐ ┌───────┐
│ 成功  │ │ 失敗  │
│ (証明)│ │ (反例)│
└───────┘ └───────┘
```

### 関連ファイル一覧

| ファイル | パス | 種別 | 役割 |
|---------|------|------|------|
| drnim.nim | `drnim/drnim.nim` | ソース | DrNimメイン実装 |
| z3_api.nim | `drnim/z3/z3_api.nim` | ソース | Z3 APIバインディング |
| guards.nim | `compiler/guards.nim` | ソース | ガード条件処理 |
| sem.nim | `compiler/sem.nim` | ソース | セマンティック解析 |
| passes.nim | `compiler/passes.nim` | ソース | コンパイラパス管理 |
| modulegraphs.nim | `compiler/modulegraphs.nim` | ソース | モジュールグラフ管理 |
