⚠️ 廃案 (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）によりメモリ安全とスレッド安全を既に保証していますが、論理的正確性はテストに依存しています。システムプログラミング、安全kritische分野（航空宇宙、金融、OSカーネルなど）では、論理的エラーが壊滅的な結果を招く可能性があります。既存のソリューション（如Rustの借用チェック）では此类エラーを検出できません。ホーア論理は数学的証明手段を提供しますが、従来の形式検証ツールは往往として独立した仕様言語と複雑な学習curveを必要とします。

現在の問題点

論理的正確性はテストでのみ検証可能で、コンパイル時に保証できない
重要なシステムコード，缺乏形式検証手段
既存の形式検証ツールは学習curveが急峻で、主流のプログラミング言語と分離している

提案

コア設計

私たちの目標は、軽量で言語と一体化した静的検証ソリューションを設計することです：

Debug Build必須検証：開発者が高い信頼性を要するモジュールに仕様を記述し、Debug Build時に強制検証を経てからRelease Buildを可能にする
elegante構文：//!コメントを使用 새キーワードを導入せず、エディタでsyntax highlighting可能
型システムとの統合：仕様が型の一部となり、型チェックに参加可能、ユーザーが仕様型を定義可能
証明可能かつテスト可能：静的証明も可能だが、実行時アサーションに退化可能、段階的な採用が容易

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. エディタサポート

//!と/*! ... !*/はエディタに認識されてspecialコメントとして識別され、異なる色（如紫）が割り当てられ、通常のコメントと区別されます。Language Serverは仕様のhover補完、補完、検証エラー報告を提供できます。

詳細設計

構文変更

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

7.1 構文拡張

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

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：関数のすべての復帰点の前にassert(cond)を挿入（resultは実際の戻り値に置換）
invariant：ループ本体の先頭にassert(cond)を挿入

7.6 既存の設計との統合

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

型システムへの影響

仕様型はYaoXiangの обычный型であり、統一構文モデルと一致
コンパイラは一般的に使用される仕様型（Positive、NonEmpty、GreaterOrEqualなど）を内置
ユーザーはобычный型定義を通じて仕様형을自定义可能
仕様型はジェネリックパラメータを帶み、型制約をサポート

実行時動作

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

コンパイラ変更

パーサー：仕様コメント構文を認識
意味解析：仕様を収集し、仕様型に変換
検証バックエンド：検証条件を生成し、SMTソルバーを呼び出し
コード生成：実行時チェックモードをサポート

後方互換性

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

权衡

利点

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

欠点

compile時間：検証モードはcompile時間を大幅に増加させる可能性がある
学習curve：効果的な仕様と量詞の記述方法を学ぶ必要がある
SMTソルバーの限界：某些複雑な特性は自動証明できない可能性がある

代替案

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

実装戦略

段階分け

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

依存関係

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

リスク

SMTソルバー統合の複雑性：Z3などのソルバーの統合は技術的な課題に直面する可能性がある
- 緩和策：成熟したRust Z3バインディングを使用し、サポートする式の種類を逐步的に расширить
検証失敗のデバッグ困難：SMTソルバーが仕様を証明できない場合、ユーザーは理由を理解しにくい
- 緩和策：明確なエラー情報と反例の説明を提供
パフォーマンスオーバーヘッド：検証モードはcompile時間を大幅に增加させる可能性がある
- 緩和策：増分検証とキャッシュメカニズムを実装

開放問題

[ ] 量詞サポート範囲：ネストされた量詞をサポートするか？高階量詞をサポートするか？
[ ] ループ不変式の推論：単純な不変式の自動推論機能を提供するか？
[ ] 証明失敗反例形式：反例を最も効果的に提示する方法は？
[ ] 他の検証ツールとの統合：Coq、Leanなどの証明アシスタントとの統合を検討するか？

参考文献

ライフサイクルと運命

┌─────────────┐
│   草案      │  ← 著者作成
└──────┬──────┘
       │
       ▼
┌─────────────┐
│  審査中     │  ← コミュニティ議論
└──────┬──────┘
       │
       ├──────────────────┐
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│  承認済み     │    │  拒否済み     │
└──────┬──────┘    └──────┬──────┘
       │                  │
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│ accepted/  │    │    rfc/     │
│ (正式設計)  │    │ (元の位置に保持)  │
└─────────────┘    └─────────────┘

ステータス説明

ステータス	位置	説明
草案	`docs/design/rfc/`	著者草案、審査提出待ち
審査中	`docs/design/rfc/`	コミュニティ議論とフィードバック公開
承認済み	`docs/design/accepted/`	正式設計ドキュメントとなり、実装段階に入る
拒否済み	`docs/design/rfc/`	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 既存の設計との統合

型システムへの影響

実行時動作

コンパイラ変更

後方互換性

权衡

利点

欠点

代替案

実装戦略

段階分け

依存関係

リスク

開放問題

参考文献

ライフサイクルと運命

ステータス説明

承認後の操作

拒否後の操作