⚠️ 廃止 (DEPRECATED)
本 RFC は RFC-027：コンパイル時評価型と統一静的検証 に置き換えられました。
廃止理由：022 は仕様を //! コメント形式のアドオン構文として設計しましたが、これは Curry-Howard 同型の根本原則に反します。「//! コメントはない。独立した仕様言語もない。すべてが型システム内にある。」新設計ではコンパイル時評価型を第一級市民とし、統一されたコンパイル時 Bool 評価パイプラインがコメント式仕様に取って代わりました。Debug/Release の分断された検証モデルも、統一された True/False/Unknown の三段階戻り値モデルに置き換えられました。
本文書は歴史的参考のためにのみ保持されています。

RFC 022: ホーア論理静的検証サポート（仕様コメントと仕様型）[廃止]

参考:
RFC-010: 統一型構文
RFC-011: ジェネリックシステム設計
RFC-009: 所有権モデル

概要

本文書では、YaoXiang 言語にホーア論理静的検証機構を導入することを提案します。これにより、開発者はコメント内に //! または /*! ... !*/ の形式で事前条件、事後条件、ループ不変条件を記述できます。Debug Build では強制的に静的検証が行われ、検証通過後にのみ Release Build が可能になります。Release Build では仕様コメントが無視され（ゼロオーバーヘッド）、検証キャッシュがクリアされます。仕様自体は型システムの一部とみなされ、「仕様型」（例：Requires(P)、Ensures(P)）を形成し、ユーザーが拡張可能です。本設計は、言語の簡潔さを保ちながら、重要なコードに対して高い信頼性保証を提供し、YaoXiang の統一型モデルと完全に融合することを目指します。

動機

なぜこの機能/変更が必要か

YaoXiang はすでに所有権モデル（RFC-009）と並行性モデル（RFC-001）によってメモリ安全性とスレッド安全性を保証していますが、論理的正しさは依然としてテストに依存しています。システムプログラミング、安全性が重要な領域（航空宇宙、金融、オペレーティングシステムカーネルなど）では、論理的エラーが壊滅的な結果をもたらす可能性があります。既存のアプローチ（Rust の借用検査など）は这类のエラーを捕捉できません。ホーア論理は数学的証明手段を提供しますが、従来の形式検証ツールは独立した仕様言語と複雑な学習曲線を必要とすることが多いです。

現在の問題

論理的正しさはテストでしか検証できず、コンパイル時には保証されない
重要なシステムコードに形式検証手段が欠如している
既存の形式検証ツールは学習曲線が急峻で、主流プログラミング言語と分断されている

提案

核心設計

我々の目標は、軽量で言語と一体化した静的検証スキームを設計することです：

Debug Build 必須検証：開発者は高信頼性が求められるモジュールに仕様を記述し、Debug Build では検証通過後にのみ Release Build が可能
構文の優雅さ：//! コメントを使用し、新しいキーワードを導入せず、エディタで色付け識別可能
型システムとの融合：仕様が型の一部となり、型検査に参加し、ユーザー定義仕様型をサポート
証明可能かつテスト可能：静的に証明することも、ランタイムアサーションに降格することもでき、段階的な採用が可能

1. 仕様コメント構文

関数本体またはループ本体の先頭で、//!（単一行）または /*! ... !*/（複数行）を使用して仕様を記述します。

1.1 統一仕様構文

仕様は YaoXiang の統一された name: Type = expression 構文モデルを採用し、型システムと完全に融合します：

yaoxiang

max: (T: Ord) -> ((arr: Array(T, n)) -> T) = {
    //! requires: NonEmpty(n) = n > 0
    //! ensures: GreaterOrEqual(result, arr[0..n])
    //! ensures: ExistsMax(result, arr[0..n])
    // 実装...
}

仕様は本質的に型宣言であり、右辺はブール式
左辺は仕様型インスタンス（型パラメータ付き可）
特別な変数 result を使用して戻り値を表現可能

1.2 ループ仕様

yaoxiang

while i < n {
    /*! invariant: Bounds[i, n] = 0 <= i <= n
                  && SumInvariant[s, arr[0..i]] ! */
    s = s + arr[i]
    i = i + 1
}

1.3 仕様式

仕様の右辺のブール式は YaoXiang 式構文を使用し、以下をサポートします：

算術演算、比較演算、論理演算
量化子：forall i in 0..n: P(i)、exists i in 0..n: P(i) — 言語組み込みの論理構造
関数呼び出し（純粋関数である必要あり）

2. 仕様型システム

仕様型は本質的に YaoXiang の通常の型であり、統一構文モデルと完全に一致しています。

2.1 組み込み仕様型

コンパイラは以下のよく使用される仕様型を組み込みで提供します（仕様内で直接使用可能）：

yaoxiang

// 組み込み仕様型定義
NonEmpty: (T: Type) -> Type = { len: T; len > 0 }
Positive: Type = { x: Int; x > 0 }
GreaterOrEqual: (T: Type) -> Type = { result: T, arr: Array(T); result >= arr[0] && forall i in 1..arr.len: result >= arr[i] }
Bounds: (T: Type) -> Type = { i: T, n: T; 0 <= i && i <= n }
SumInvariant: (T: Type) -> Type = { s: T, arr: Array(T); s == sum(arr[0..i]) }

// 量化子構造（言語組み込み、関数ではない）
forall: (start: Int, end: Int, pred: (Int) -> Bool) -> Bool
exists: (start: Int, end: Int, pred: (Int) -> Bool) -> Bool

2.2 ユーザー定義仕様型

通常の型定義と完全に一致しており、ユーザーは仕様型をカスタム定義できます：

yaoxiang

// 正整数仕様の定義
Positive: Type = { x: Int; x > 0 }

// ソート済み配列仕様の定義
Sorted: (T: Ord) -> Type = {
    arr: Array(T);
    forall i in 0..arr.len-1: arr[i] <= arr[i+1]
}

// 最大値仕様の定義
ExistsMax: (T: Ord) -> Type = {
    result: T, arr: Array(T);
    exists i in 0..arr.len: result == arr[i]
    && forall j in 0..arr.len: result >= arr[j]
}

カスタム仕様の使用：

yaoxiang

sqrt: (x: Positive) -> Float = {
    //! ensures: SquareRootResult(result, x) = result * result <= x && (result+1)*(result+1) > x
    // 実装...
}

binary_search: (T: Ord) -> ((arr: Sorted(Array(T)), key: T) -> Option(Index)) = {
    //! ensures: SearchResult(result, arr, key)
    // 実装...
}

仕様型は他の型と同様に、ジェネリックパラメータ、型制約をサポートし、型推論に参加できます。

3. コンパイルモード

モード	動作	オプション
Debug Build	仕様を解析し、検証条件を生成し、SMT ソルバーを呼び出して証明；検証通過後にのみ Release Build が可能	`yaoxiangc --debug source.yx`
Release Build	すべての `//!` コメントを無視し、コードを生成しない；すべての検証キャッシュをクリア；積極的最適化を有効化	`yaoxiangc --release source.yx`
ランタイムチェック	仕様をランタイムアサーションに変換し、違反時に panic	`yaoxiangc --enable-runtime-checks source.yx`

検証モードで証明が失敗した場合、コンパイラはエラーを報告し、可能な反例（入力値など）を提示します。

4. 検証機構

コンパイラは仕様を検証条件（Verification Conditions）に変換し、統合された SMT ソルバー（例：Z3）に送信します。検証プロセスは概ね以下の通りです：

関数の requires と ensures、ループの invariant を収集
各ループについてループ不変式証明義務を生成：ループ進入前に成立、各イテレーション後に保持、ループ終了後に事後条件を含意
関数本体を論理式に変換し、仕様と組み合わせて検証条件を生成
SMT ソルバーを呼び出して充足可能性をチェック

ソルバーが unsat（充足不能）を返した場合、仕様は成立します；それ以外の場合は反例を報告します。

5. テストとの結合

ランタイムチェックモードは仕様をアサーションに変換し、テストに使用できます。仕様カバレッジツールと組み合わせることで、テストによる仕様のカバー度を評価できます。将来的には、テストから候補仕様を自動推論する仕様マイニングツールを検討する可能性があります。

6. エディタサポート

//! と /*! ... !*/ はエディタで特殊コメントとして認識され、異なる色（例：紫色）が付与され、通常のコメントと区別されます。言語サーバーは仕様のホバー表示、补完、検証エラー報告を提供できます。

詳細設計

構文変更

以前	以後
仕様コメント構文なし	`//!` および `/! ... !/` 仕様コメントを許可

7.1 構文拡張

既存構文（RFC-010）基础上、関数本体とループ本体の先頭にゼロ個以上の //! または /*! ... !*/ コメントの出現を許可します。仕様構文は統一型構文と一致しています：

spec_comment     ::= ('//!' spec_line) | ('/*!' spec_block '!*/')
spec_line        ::= spec_name ':' type_expr '=' expr
spec_name        ::= 'requires' | 'ensures' | 'invariant'
spec_block       ::= (spec_name ':' type_expr '=' expr ';')*

仕様は本質的に型宣言：仕様名: 仕様型 = ブール式
type_expr は仕様型式、型パラメータ付き可
expr は YaoXiang 式構文を使用し、量化子をサポート

7.2 型検査

検証モードでは、コンパイラは仕様コメントを対応する仕様型インスタンスに変換し、関数またはループのメタデータに記録します。

7.3 検証条件生成

weakest precondition または strongest postcondition 演算法を採用し、ループ不変式と組み合わせて一階論理式を生成します。生成された VC は SMT-LIB 形式を使用し、外部ソルバーを呼び出します。

7.4 エラー報告

証明が失敗した場合、ソルバーはモデル（反例）を提供する可能性があります。コンパイラはこれらの反例を、たとえば具体的な入力値など、人間が読める形式に変換し、ユーザーのデバッグを支援する必要があります。

7.5 ランタイムチェック

--enable-runtime-checks モードでは、コンパイラは仕様を assert 文に変換します：

requires：関数入口に assert(cond) を挿入
ensures：関数のすべての return ポイントの前に assert(cond) を挿入、result は実際の戻り値に置き換え
invariant：ループ本体の先頭に assert(cond) を挿入

7.6 既存設計との統合

所有権モデル：仕様内の式は所有権規則に従い、読み取りのみで書き込み不可（純粋関数）であり、副作用を回避
ジェネリックシステム：仕様型はジェネリックパラメータをサポート（例：Requires(P)）、ジェネリック関数/型と組み合わせ可能
依存型：仕様内の値依存型（例：配列の長さ n）は自然に利用可能

型システムへの影響

仕様型は YaoXiang の通常の型であり、統一構文モデルと一致
コンパイラはよく使用される仕様型（Positive、NonEmpty、GreaterOrEqual など）を組み込みで提供
ユーザーは通常の型定義を通じてカスタム仕様型を定義可能
仕様型はジェネリックパラメータを取れ、型制約をサポート

ランタイム動作

Debug Build：SMT ソルバーを呼び出して静的検証を行い、コンパイル時間が増加；検証成功後に結果をキャッシュ
Release Build：仕様コメントは無視され、ランタイムオーバーヘッドはゼロ；すべての検証キャッシュをクリア；Span キャッシュクリアなどの積極的最適化を有効化
ランタイムチェックモード：assert 文を生成し、ランタイムで違反を検出

コンパイラの改修

パーサー：仕様コメント構文を認識
セマンティック分析：仕様を収集し、仕様型に変換
検証バックエンド：検証条件を生成し、SMT ソルバーを呼び出し
コード生成：ランタイムチェックモードをサポート

後方互換性

✅ 完全後方互換
通常コンパイルでは仕様コメントが無視され、既存コードに影響しない
Release Build では仕様が無視され、余分なオーバーヘッドなし

トレードオフ

利点

Debug Build 検証：Debug Build 時に強制検証し、論理的正しさを保証
構文の優雅さ：純粋なコメント、新しいキーワードなし、エディタフレンドリー
型システムとの融合：仕様は型であり、拡張可能
段階的採用：ランタイムチェックから段階的に静的検証へ移行可能
信頼性向上：テストでは発見しにくい論理的エラーを捕捉可能

欠点

コンパイル時間：検証モードはコンパイル時間を大幅に増加させる可能性
学習曲線：効果的な仕様と量化子の記述方法を学ぶ必要
SMT ソルバーの限界：複雑な性質の中には自動証明できないものがある可能性

代替案

案	利点	欠点
新しいキーワード（例：`requires`）	構文が直感的	新しいキーワードを導入し、簡潔性を損なう
独立した仕様ファイル（例：CVL）	仕様とコードが分離	ファイル数増加、同期が困難
ランタイムアサーションのみ	実装が簡単	静的に保証できない
本提案（コメント+仕様型）	簡潔さと機能性のバランス	エディタサポートが必要

実装戦略

段階区分

段階	内容
段階 1：基礎サポート	パーサーを拡張し、`//!` および `/! ... !/` コメントを認識して AST ノードに付加；検証モードで仕様を収集し、単純な検証条件（算術比較のみ）を生成；Z3 ソルバーを統合
段階 2：量化子サポート	量化子式をサポートし、SMT-LIB の `forall`/`exists` に変換；仕様の IDE ハイライトとホバー表示を提供
段階 3：最適化とツールチェーン	増分検証、検証済みモジュールのキャッシュ；仕様カバレッジレポート；仕様マイニングツール（テストから候補仕様を生成）

依存関係

RFC-009: 所有権モデル - 仕様式は純粋関数セマンティクスを必要とする
RFC-010: 統一型構文 - 仕様型システムは型システムに基づく
RFC-011: ジェネリックシステム設計 - 仕様型はジェネリックパラメータをサポート

リスク

SMT ソルバー統合の複雑さ：Z3 などのソルバーの統合は技術的課題に直面する可能性
- 緩和策：成熟した Rust Z3 バインディングを使用し、サポートする式タイプを段階的に拡張
検証失敗のデバッグ困難さ：SMT ソルバーが仕様を証明できない場合、ユーザーがその原因を理解しにくい
- 緩和策：明確なエラーメッセージと反例の説明を提供
パフォーマンスオーバーヘッド：検証モードはコンパイル時間を大幅に増加させる可能性
- 緩和策：増分検証とキャッシュ機構を実装

未解決問題

[ ] 量化子サポート範囲：ネストした量化子をサポートするか？高階量化子をサポートするか？
[ ] ループ不変式推論：単純な不変式を自動推論する機能を提供するか？
[ ] 証明失敗反例フォーマット：反例を最も効果的に提示する方法は？
[ ] 他の検証ツールとの統合：Coq、Lean などの証明支援ツールとの統合を検討するか？

参考文献

ライフサイクルと归宿

┌─────────────┐
│   草案      │  ← 作者が作成
└──────┬──────┘
       │
       ▼
┌─────────────┐
│  レビュー中     │  ← コミュニティで議論
└──────┬──────┘
       │
       ├──────────────────┐
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│  採用済み     │    │  拒否済み     │
└──────┬──────┘    └──────┬──────┘
       │                  │
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│ accepted/  │    │    rfc/     │
│ (正式設計)  │    │ (元の位置を保持)  │
└──────┬──────┘    └──────┬──────┘
       │                  │
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│ 廃止/置換 │    │  保持（参考）  │
└─────────────┘    └─────────────┘

状態説明

状態	位置	説明
草案	`docs/design/rfc/`	作者による草稿、レビュー待ち
レビュー中	`docs/design/rfc/`	コミュニティでの議論とフィードバックを公開中
採用済み	`docs/design/accepted/`	正式設計文書となり、実装段階に移行
拒否済み	`docs/design/rfc/`	RFC ディレクトリに保持され、状態を更新
廃止	`docs/design/rfc/` または `docs/design/accepted/`	後の RFC により置き換え済み、参照用として保持

採用後の操作

RFC を docs/design/accepted/ ディレクトリに移動
ファイル名を説明的な名前に更新（例：hoare-logic-static-verification.md）
状態を "正式" に更新
状態を "採用済み" に更新し、採用日を追加

拒否後の操作

docs/design/rfc/ ディレクトリに保持
ファイル先頭に拒否理由と日付を追加
状態を "拒否済み" に更新

RFC 022: ホーア論理静的検証サポート（仕様コメントと仕様型）[廃止] ​

概要 ​

動機 ​

なぜこの機能/変更が必要か ​

現在の問題 ​

提案 ​

核心設計 ​

1. 仕様コメント構文 ​

1.1 統一仕様構文 ​

1.2 ループ仕様 ​

1.3 仕様式 ​

2. 仕様型システム ​

2.1 組み込み仕様型 ​

2.2 ユーザー定義仕様型 ​

3. コンパイルモード ​

4. 検証機構 ​

5. テストとの結合 ​

6. エディタサポート ​

詳細設計 ​

構文変更 ​

7.1 構文拡張 ​

7.2 型検査 ​

7.3 検証条件生成 ​

7.4 エラー報告 ​

7.5 ランタイムチェック ​

7.6 既存設計との統合 ​

型システムへの影響 ​

ランタイム動作 ​

コンパイラの改修 ​

後方互換性 ​

トレードオフ ​

利点 ​

欠点 ​

代替案 ​

実装戦略 ​

段階区分 ​

依存関係 ​

リスク ​

未解決問題 ​

参考文献 ​

ライフサイクルと归宿 ​

状態説明 ​

採用後の操作 ​

拒否後の操作 ​

RFC 022: ホーア論理静的検証サポート（仕様コメントと仕様型）[廃止]

概要

動機

なぜこの機能/変更が必要か

現在の問題

提案

核心設計

1. 仕様コメント構文

1.1 統一仕様構文

1.2 ループ仕様

1.3 仕様式

2. 仕様型システム

2.1 組み込み仕様型

2.2 ユーザー定義仕様型

3. コンパイルモード

4. 検証機構

5. テストとの結合

6. エディタサポート

詳細設計

構文変更

7.1 構文拡張

7.2 型検査

7.3 検証条件生成

7.4 エラー報告

7.5 ランタイムチェック

7.6 既存設計との統合

型システムへの影響

ランタイム動作

コンパイラの改修

後方互換性

トレードオフ

利点

欠点

代替案

実装戦略

段階区分

依存関係

リスク

未解決問題

参考文献

ライフサイクルと归宿

状態説明

採用後の操作

拒否後の操作