code-contracts

コードコントラクト

コードと同じ場所に配置された構造化された前提条件と要件を指定するためのシンプルなオープン形式です。エージェント主導のソフトウェア開発を、より迅速かつ効果的に進めることを支援します。

/**
 * @cc [owner:spolu,label:product] balance-pre-and-fail
 * `from.balance` is expected to be greater than or equal to `invoice.amount`, fails with
 * `InsufficientBalanceError` otherwise.
 */
/**
 * @cc [owner:spolu,label:product] balance-post
 * `from.balance` is decreased by `invoice.amount` and `invoice.status` is set to `paid`.
 */
/**
 * @cc [owner:spolu,label:product] atomicity
 * The operation is atomic: either `from.balance` is decreased and `invoice.status` is set to
 * `paid`, or neither is changed.
 */
export async function payInvoice(
  invoice: Invoice,
  from: Account,
): Promise<PaidInvoice> {
 ...
}

コードコントラクトが必要な理由

コードコントラクトは、人間とエージェントの双方がコードについて推論するために記述し、使用します。

主に3つの役割があります。

仕様：コードとは別のプロダクトやシステムの仕様ファイルは、コードとの乖離が起きやすく、見つけにくい傾向があります。一方、コードコントラクトはコードの近くに埋め込まれています。人間は実装の詳細を調べずに動作について推論でき、エージェントは実装の指針として利用し、重要な前提条件を人間や将来のエージェントに提示できます。

注意：重要な前提条件と不変条件を構造化された形式で提示することで、コードについて推論するために必要なサイクルを減らします。これにより、現代のソフトウェア開発チームにおいて最もボトルネックになりやすいリソースの1つである、人間の注意力を節約できます。

検証：構造と粒度により、ツールを使って準拠状況を強制し、長期にわたる保守を容易にできます。コードコントラクトの準拠状況を強制することで、エージェントに検証シグナルを提供し、そのパフォーマンスを向上させます。

コードコントラクトにより、次のことが可能になります。

• 人間の開発者とコーディングエージェントの連携をより効率化できます。
• エージェントのパフォーマンスを向上させる、生成型コード分析と検証を実現できます。
• コードレベルで不変条件、プロダクトコントラクト、セキュリティ上の前提条件を大規模に保守できます。

ツール

npm install --global @spolu/cc-check

cc-check コマンドラインインターフェースでは、次の操作を実行できます。

• cc-check format [file-like]：サポート対象のソースファイルまたは CONTRACTS ファイルにある、不正な @cc 構文と重複したコントラクト ID を報告します。パスを指定しない場合は、現在のディレクトリ内にあるサポート対象のすべてのファイルを再帰的に調べます。ファイルを書き換えたり、コントラクトの文章や実装の準拠状況を評価したりすることはありません。
• cc-check list <file-like|location-like>：サポート対象のソースファイル内で宣言に関連付けられたコントラクトを一覧表示するか、ソース位置を含む宣言とその宣言の祖先に適用されるコントラクトを一覧表示します。祖先にある CONTRACTS ファイルのディレクトリスコープのコントラクトは、既定で含まれます。除外するには --no-global を指定します。

cc-check format
cc-check format path/file.rs
cc-check list path/to/file.ts:42
cc-check list path/to/file.go

仕様と文法

@cc ディレクティブは、サポートされている任意のソース言語のドキュメントコメントから抽出されます。各ディレクティブは、1つのコード契約を定義します。契約は通常、関数、クラス、またはメソッドの定義と同じ場所、またはその内部に記述されます。

宣言に紐付いていないコード契約は、CONTRACTS という名前のファイルに記述します。そのファイルが置かれたディレクトリと、その配下のディレクトリに含まれるすべてのコードに適用されます。一般的な用途は、アーキテクチャ上の境界、依存関係の制約、セキュリティ対策など、ディレクトリ単位のコーディングルールを定めることです。

CONTRACTS ファイルの例：

@cc [owner:spolu,label:architecture] database-access-thru-resources
Database accesses must happen exclusively through `Resource`-like interfaces.

@cc [owner:spolu,label:security] no-sensitive-data-logging
Credentials, tokens, secrets and user data must not be logged.

文法には ISO 形式の EBNF を使用します。SP は1つ以上のスペース、NL は改行です。解析の前に、/**、*/、//、///、Python のドキュメント文字列の三重引用符、行頭の * などのコメント区切り文字と装飾は取り除かれます。

contracts_file
              = { contract, NL } ;
contract      = directive, NL, prose ;
directive     = "@cc", SP, [ metadata, SP ], contract_id ;

metadata      = "[", attribute, { ",", attribute }, "]" ;
attribute     = key, ":", value ;

contract_id   = token ;
key           = token ;
value         = token ;
prose         = prose_line, { NL, prose_line } ;

token は、空白、カンマ、コロン、角括弧を含まない空でない文字列です。メタデータキーは拡張可能で、owner、notify、label がよく使われるキーです。1つの契約に複数のオーナー、通知先、ラベルを指定できます。属性キーを繰り返す代わりに、属性内の値を区切るには ; を使用してください。たとえば、[owner:spolu;tdraier,label:product] は [owner:spolu,owner:tdraier,label:product] の代わりに使用できます。複数のラベルを指定する場合は、label:product;security とします。同じキーの繰り返しも有効です。セミコロン区切りのリストはメタデータの規約であり、パーサーは各値を単一のトークンとして保持します。prose_line は、@cc ディレクティブで始まらない任意の行です。

owner には、既存の契約が変更または削除されたときに通知する GitHub ユーザー名を列挙します。契約の追加時にはオーナーに通知されません。notify には、その契約に違反していることが検出されるたびに通知する GitHub ユーザー名を列挙します。 たとえば、[owner:spolu,notify:spolu;flvndvd,label:product] の場合、契約の変更については spolu に通知し、違反については spolu と flvndvd の両方に通知します。オーナーには違反が自動的に通知されません。両方の通知を希望する場合は、オーナーを notify に含めてください。レビューエージェントはセミコロン区切りのリストを分割し、同じキーを統合したうえで、重複するユーザー名を除外します。

説明本文は空であってはならず、ドキュメントコメントの末尾、CONTRACTS ファイル内の次の @cc ディレクティブ、またはそのファイルの末尾まで続きます。任意のテキストを含めることができ、行数に制限はありません。コア形式では、語彙、文の形式、法性、要件の表記法を規定していませんが、一般に Markdown が想定されています。

ドキュメントコメントには @cc ディレクティブを1つ含めます。複数の契約コメントを連続して記述し、同じ宣言に紐付けることもできます。契約 ID は、紐付けられた宣言内で一意かつ安定している必要があります。同じ ID を別の宣言に使用してもかまいません。CONTRACTS ファイル内の契約は宣言に紐付いておらず、そのファイル内とすべての親 CONTRACTS ファイルを通じて、ID は一意かつ安定している必要があります。

宣言に紐付いた契約の識別子は、その宣言の言語固有の識別子と契約 ID の組み合わせです。ディレクトリ契約の識別子は、その CONTRACTS ファイルのリポジトリ相対パスと契約 ID の組み合わせです。

コード契約のワークフロー

$code-contracts verify を実行する場合は、オンデマンド検証に従ってください。

契約の検出

コードを変更またはレビューする前に、対象に適用されるローカル契約、宣言を囲む契約、祖先ディレクトリの CONTRACTS ファイルに記述された契約をすべて特定してください。手動で行うか、cc-check list を使用します。呼び出されるシンボルを特定し、その契約も確認してください。別のファイルで宣言された契約に、呼び出しが違反する場合があります。

適用されるすべてのローカル契約とディレクトリ契約を、同時に満たすべき要件として扱ってください。矛盾している、古くなっている、または実現不可能な契約があれば、黙っていずれかを選ばず、明らかにしてください。ドキュメントの例や、意図的に不正な形式にしたテスト用フィクスチャは、本番用の契約宣言ではありません。

コントラクトの記述

コードコントラクトは、シンプルで簡潔かつ正確な場合に効果を発揮します。宣言固有のコントラクトは、その言語でサポートされているドキュメントコメントまたは docstring に記述します。ディレクトリツリーを対象とするコントラクトは、通常、アーキテクチャ、セキュリティ、またはコーディング上の制約について CONTRACTS に記述します。関連する宣言またはディレクトリの境界のうち、最も狭いものを使用します。

各ソースドキュメントブロックには、コントラクトをちょうど1つ記述します。宣言内でコントラクト ID を一意かつ安定したものに保ちます。CONTRACTS の ID は、そのファイル内および親の CONTRACTS ファイル内で一意かつ安定したものに保ちます。owner には現在のユーザーの GitHub ユーザー名を設定します。認証済みの GitHub ID が利用できる場合はそれを使用し、特定できない場合は推測せずに尋ねます。複数のオーナーを指定できます。1つの owner 属性内で、ユーザー名を ; で区切ることを推奨します。複数のラベルと notify の宛先にも同じ規則を使用します。notify を設定するのは、ユーザーから明示的に依頼された場合に限ります。owner から推測してはいけません。リポジトリで確立されているメタデータの規則を維持します。

cc-check format でコントラクトの構文を検証します。このコマンドが報告するのは、不正な構文と重複 ID のみです。記述内容が真実であることや、コードがコントラクトに準拠していることを証明するものではありません。コントラクトの妥当性と一貫性、およびコードの準拠状況は、自分で確認する責任があります。cc-check list でコントラクトの見つけやすさを検証します。

各コントラクトは、具体的な義務を中心に記述します。

• 防止するリグレッションを特定します。 要件に違反する可能性のある変更を具体的に示します。関数の目的を説明するだけの記述は、通常のドキュメントに記載します。
• 観測可能な要件を示します。 「［条件のもとで、］対象は要件を満たさなければならない／満たしてはならない」の形式を推奨します。直接的な不変条件も同様に有効です。規範的なキーワードを使うだけでは、記述は正確になりません。
• 独立した義務は分けます。 要件ごとにコントラクトを1つ記述します。1つの要件を定義する条件付きのケースは、同じコントラクトに含めてもかまいません。
• 判断に必要なケースを明示します。 コンプライアンスの判定に影響する場合は、データが欠落したときの動作、フォールバック、エラー、副作用を含めます。結果がないことと、結果を取得できないことを区別します。
• 境界を正確に指定します。 関連する入力、出力、フィールド、状態、または効果を特定します。「ワークスペース全体」などの表現は、意図する場合、明示的な前提条件または保証として定義します。
• 実装を変えても意図を維持します。 実際の制約を課さない限り、目的、根拠、アルゴリズムの説明は省きます。意図を裏付ける根拠なしに、実装上たまたま見られる動作を要件にしてはいけません。

コントラクトを残す前に、レビュー担当者が具体的な違反例と、それを満たす別の実装の両方を特定できることを確認します。

コントラクトの遵守

コード変更に関連して見つかった、または新たに導入されたすべてのコントラクトが、常に有効で、一貫性があり、適用され、遵守されていることを確認する必要があります。コントラクトを意味的に自動検証する仕組みはありません。コード変更は、該当するすべてのコントラクトに準拠しているものとみなされるため、作成者とレビュー担当者がその準拠を確認する必要があります。

タスクの対象範囲内にあるコントラクト違反や矛盾は修正するか、明確に指摘する必要があります。レビューでは、オンデマンド検証に従ってください。

動作を意図的に変更する場合は、同じ変更内で該当するコントラクトを更新してください。コントラクトの変更が、関連する宣言の利用者に与える影響を確認してください。

すべてのコード変更に関する重大な要件

• 技術設計を決める前に、該当するコントラクトを見つけて確認してください。
• 新しい動作に関係するコントラクトを導入してください。
• 既存コードについて重要な前提を置く場合は、欠落しているコントラクトを補ってください。
• 重要な変更を行うたびに、実装、関連するテスト、コントラクトの記述内容が一致するように調整してください。
• 動作を意図的に変更する場合、その仕様変更が対象範囲内であれば、同じ変更内でコントラクトを更新してください。
• 実装を準拠しているように見せるために、コントラクトを削除したり弱めたりしてはいけません。
• コードとコントラクトの不一致は指摘事項として扱ってください。修正するか、明確に指摘してください。どちらか一方が自動的に正しいとみなしてはいけません。

オンデマンド検証

$code-contracts verifyとして呼び出された場合、またはレビュー手順でこの手順が求められた場合は、読み取り専用のコントラクトレビューを実施してください。該当するリポジトリの指示を読み、別途依頼されない限り、ファイルの編集、レビューの投稿、通知の送信は行わないでください。

指定されたPR、リビジョン範囲、ファイル、ディレクトリ、またはリポジトリを対象範囲として使用してください。対象範囲が明示されていない場合は、コミット済みのブランチ変更と、ステージ済み、未ステージ、未追跡のファイルを含め、現在のタスクの変更をレビューしてください。タスクまたはリポジトリの状況からブランチの比較ベースを推測してください。対象またはベースラインを特定できない場合は、対象範囲を尋ねてください。ファイルまたはディレクトリは、差分がなくても現在のコントラクトに照らして検証できます。手順で保存済みのコミットが指定されている場合は、ブランチが進んでいても、その正確な比較を使用してください。

差分との関連性。 変更を、該当するすべてのコントラクトに照らして確認してください。変更されていないコードも調査し、既存の違反は、変更された動作、変更が依拠する前提、または新規もしくは変更されたコントラクトに直接関連する場合に限って報告してください。該当する理由を指摘事項で説明してください。同じファイル、宣言、または呼び出しグラフに含まれるだけでは、関連性があるとはいえません。このルールは、以前のレビューから引き継がれた指摘事項にも適用されます。

差分のない監査では、選択された対象範囲全体を確認してください。

1. 差分と周辺の実装を確認します。差分がない場合は、選択されたコード全体を確認します。 コミットを比較する場合は、git diff --find-renames <merge_base> <head_sha> と、 古いコードや契約を確認するための git show <merge_base>:<path> を使用します。対象範囲に含まれるローカル変更も確認します。 提供されたファイル一覧が途中で切れている場合でも、ローカルで変更ファイルを特定します。追加、変更、削除による影響を確認します。 契約の本文とメタデータ全体を比較します。追加された @cc 行だけを検索すると、文章のみの変更や削除された契約を見落とします。
2. 対象コードに対して契約の発見を適用します。関連する契約の構文を cc-check format で検証します。このコマンドが確認するのは構文であり、意味上の妥当性や準拠性ではありません。 呼び出し元から cc-check 実行ファイルが提供されている場合は、それを使用します。ツールを利用できない場合は、契約を手作業で確認し、その結果生じた検証上の制限を明示します。
3. 各コード要素を、適用される契約と照合します。実際の入力、ガード、エラー、出力、状態変更、副作用を追跡します。契約が有効か、実装や他の適用対象の契約と整合しているかを確認します。矛盾や、証拠によって裏付けられる不一致を報告します。コードも契約も自動的に正しいとは見なしません。同じ変更で契約が弱められたり削除されたりしたことを、違反の理由として認めてはいけません。意図的で一貫した仕様変更と、隠れたリグレッションを区別します。
4. 新規追加、変更、または明示的に対象とされた契約すべてについて、前述の関連性の基準に従い、実装する宣言とその利用箇所（変更されていない呼び出し元を含む）を調べます。rg とソースコードのナビゲーションで呼び出し元や参照箇所を特定します。インポート、再エクスポート、別名、ラッパー、型やメンバーの使用を追跡し、各一致箇所が対象の宣言を参照していることを確認します。ディレクトリ契約の場合は、そのサブツリー内の該当コードと、影響を受ける宣言の利用箇所を調べます。
5. 調査した各呼び出し元・参照箇所で、cc-check list <caller-location> を使うか手作業で確認し、それぞれに適用される契約を特定します。呼び出しが呼び出し先の契約を守っていることと、呼び出し先で変更された保証によって呼び出し元自身の契約への準拠が維持されていることの両方を確認します。ラッパーを通じた証拠も追跡し、利用側が互換だと決めつけてはいけません。
6. 影響を受ける各宣言について、異なる呼び出し元・参照箇所を最大64件まで調べます。重複する呼び出し元・参照箇所はまとめます。変更された呼び出し元、リスクの高い動作、多様な使用パターンを優先します。この上限は、呼び出し元を通じた追加調査にも適用します。呼び出し元の件数、未調査の範囲、検索上の制限、不確かな関係を作業分析に記録します。結論に重大な影響を与える制限は、該当する場合、関連する指摘とともに明示します。上限に達した場合や調査が妨げられた場合に、網羅的に検証したと誤解させてはいけません。

調査対象のリビジョンに対する、適用可能な検証結果を再利用します。サンドボックスの制限を守ります。ツールを利用できないことや失敗したことだけを、契約違反の証拠として扱ってはいけません。ソースの分析を続け、重大な検証上の制限を報告します。

指定がある場合は、呼び出し元のワークフローで定められた出力形式を使用します。指定がない場合は、契約 ID と宣言・ファイル、ソース内の正確な位置、証拠、影響を含め、簡潔な指摘を報告します。以前から存在する違反はその旨を示し、推測に基づくものや無関係な一般的レビュー指摘は避けます。違反が見つからない場合は、重大な制限があればそれも添えて、調査対象の範囲では違反がなかったことを明記します。