maintain-formal-verification-skill

形式検証スキルを保守する

形式チェックは、記述対象の性質を証明します。コードが変更されても検証が更新されなければ、すでに存在しないコードを記述したままチェックに合格し続けることがあります。合格しているために証明のように見えるこの状態は、危険です。このスキルは、create-formal-verification-skillスキルが生成した検証スキル、または名前が指定されたコードに対してモデルチェッカー、証明器、あるいはコードレベルの検証器を実行する、プロジェクト固有のスキルを保守するためのループです。プロジェクト固有のスキルは、エージェントがそのスキルを使っている間に行う変更に対応します。このスキルは、そのスキルを使わずに行われた変更、つまりマージ、スキルを使わずに行われた編集、そして多くのコミットにわたって蓄積する乖離に対応します。

成果

各チェックにひとつの結果を付け、どれに当たるかを明記してください。

• 同期済み：前回の同期以降、チェックの記述対象を変える変更はなく、チェックに合格します。
• 更新済み：コードが変更され、検証が新しいコードを記述するようになり、チェックに合格します。
• バグ：検証は現在のコードを記述しており、コードが性質を満たしていません。これはコードに関する指摘であり、乖離ではありません。
• ブロック：チェックを元の状態に戻せなかった、または実行できませんでした。理由を正確に述べてください。

チェックは「更新済み」と「バグ」の両方に該当することがあります。更新によって検証が再びコードを記述するようになり、そのコードに対して性質が満たされない場合です。

編集範囲

編集対象は、モデル、ハーネス、プロパティファイル、そして検証スキル自体に限ってください。ユーザーから依頼がない限り、実行中に製品コードを編集してはいけません。現在のコードに対してプロパティが失敗した場合、合格させるためにプロパティやモデルを弱めてはいけません。失敗を報告してください。

合格

1. チェックを見つけます。 検証スキルに決まった名前はないため、何をするかを手がかりに見つけてください。名前が付いたコードに対してモデルチェッカー、定理証明器、または別の検証ツールを実行する、プロジェクトのスキルです。見つかったものをすべて、またはユーザーが指定したものを読みます。各チェックについて、検証する性質、対象となるコード、境界と前提条件、実行コマンド、およびコードを説明していることが最後に確認されたコミットを記録します。検証スキルが存在しない場合は、作業を止めて /create-formal-verification-skill を案内します。スキルに同期コミットが記録されていない場合は、検証ファイルを最後に変更したコミットを使い、その旨を明記します。

2. 現状のまま実行します。 変更を加える前に各チェックを一度実行し、結果を記録します。ここで合格しても、コードが正しいとは分かりません。分かるのは、以前の説明が依然として当てはまるということです。ここでの失敗は、乖離かバグの可能性があります。手順 5 までは、どちらかを判断しないでください。

3. 対象コードへの変更をすべて読みます。 同期コミットから現在のコミットまで、対象ファイルの差分を確認し、各コミットメッセージを読みます。また、移動したコードも探します。対象の関数が名前変更、分割、または別ファイルへ移動されていても、引き続き対象コードです。さらに、チェックが保護する状態に触れる新しいコードも探します。たとえば、同じフィールドを書き込む新しい関数などです。各変更を次のいずれかに分類します。

   • 影響なし。 書式、コメント、または検証で対象としていないコードパスなど、変更が検証の記述対象に影響しません。コミットメッセージではなく、モデルまたはハーネスに照らして確認します。
   • 検証がコードを説明しなくなった。 それまで分割できない一つのアクションだったものが二つになった、分岐が追加または削除された、チェックが移動した、保護対象の状態に到達する新しい経路が追加された、または値の範囲が変わった場合です。モデルまたはハーネスを変更する必要があります。
   • 意図的に保証内容が変わった。 コードが保証する内容を変更し、その意図が変更の証拠に示されています。証拠には、ドキュメントコメント、テスト、変更履歴、またはコミットメッセージがあります。性質を変更し、その証拠を引用する必要があります。
   • 保証が破られた可能性がある。 コードが変更されたものの、保証内容が変わったことを示す証拠がありません。これに続いて失敗した場合は、バグ候補として扱います。

4. 結果ではなくコードを基に更新します。 変更された各部分が、レビュアーが開いて確認できるコードを再び指すように、モデルまたはハーネスを変更します。また、コード内の分割できない一つのステップは、検証でも一つのステップとして扱います。再実行する前にコードを基に更新し、チェックに合格させるための変更はしないでください。性質を変更するのは、保証内容が意図的に変わった場合だけです。以前の記述、新しい記述、その証拠を記録します。境界は、変更によって不適切にならない限り維持します。境界を縮小しなければならない場合は、レポートにその旨を記載します。

5. 再実行し、結果を判断します。

   • 合格： チェックが、失敗を検出できなくなった説明に対しても合格する可能性があります。新しいチェックを削除する、新しいステップの順序を変えるなど、性質が保護する方法で新しいコードに問題を起こし、チェックがそれを検出することを確認します。その後、問題を起こした変更を元に戻します。
   • 失敗： 反例を実際のコードで、一つずつ再現します。あるステップがコード上で起こり得ない場合、検証が誤っています。検証を修正し、何が誤っていたかを記載します。すべてのステップが起こり得る場合は、バグです。バグを導入したコミットを特定し、コード自体の用語を使って一連のステップとして反例を説明し、被害を一文で述べます。実際のコードに対する簡単なテストや再現でバグを確認できる場合は、証拠としてレポートに追加します。製品コードにはコミットしないでください。

6. 検証スキルを更新します。 各チェックが対象とするコード、コマンド、境界、前提条件、および同期コミットを更新します。同期コミットには、確認したコミットを設定します。ブロックされたチェックの同期コミットは移動せず、その旨をレポートに記載します。その後、次のエージェントが行うように検証スキルを一度実行し、手順が引き続き動作することを確認します。

レポート

各チェックについて、ユーザーに以下を伝えます。

• 結果と、確認したコミット
• 検証内容を何のために、どのように変更したか。それぞれの変更について、コードの形が変わったためなのか、根拠を示したうえで意図的に仕様を変更したためなのかを、簡潔に説明します。
• 再実行の結果と、更新後のチェックでも失敗することを示すために使用した破壊的変更
• 各バグの内容をわかりやすく説明します。コード上の用語を使った反例の手順、被害の内容、バグを持ち込んだコミットを記載します。
• 新しいコードを含め、検証でまだカバーできていない範囲

検証のずれとコードのバグのどちらによる失敗なのかを、明確に示します。更新前はパスし、更新後に失敗するチェックについては、以前のパスは古い記述に基づくものだったと説明します。

検証の更新は、製品の修正とは別の変更としてコミットします。