正確性オラクル は何をしますか?
約束された振る舞いを反証できる観測手段を選択します。成功したチェックが何を未テストのまま残すかを明確にしてください。カウント比較、構造チェック、依存関係の証拠はそれぞれ異なる特性を観測します(NoREC実装、SQLite整合性チェック、Elle §4.3)。
実際の境界からチェックを導出する
ターゲットの有効な設定、公開プロデューサー、統治契約を読み解きます。合法的な開始状態、操作の事前条件、許可されたエラー、約束された境界(1つの操作、ステートメント、トランザクション、リカバリ、または観測された履歴)を特定します。SQLiteでは、ABORTは1つのステートメントを元に戻しますが、遅延外部キーは「トランザクションがCOMMITを試みるまでチェックされません」(SQLite ABORT、遅延外部キー)。可能な場合は有効な設定をクエリします。たとえば、SQLiteの外部キー設定は「トランザクション内ではノーオペレーションです」(SQLite foreign_keys)。
探索を拡大する前に、具体的な候補観測を記述します。
- 約束: 正確な禁止結果または影響(契約の引用付き)。
- 観測: その違反を許可された動作から区別する、実際の返却コンテンツ、状態、または証拠。
- 事前条件とブラインドスポット: サポートされる設定、有効な状態、省略された情報、区別不可能な実行。
- 再生証拠: 入力と初期状態、操作シーケンス、有効な設定、生の観測データ。
これはコンパクトな設計規約であり、必須のスキーマではありません。その目的は、提案されたチェックによって失われる情報を明らかにすることです。Elleの観測モデルは、隠れた依存関係が単により多くの履歴を生成しても回復できない理由を示しています。つまり、ブラインドレジスタ書き込みは「履歴を破壊する」のです(Elle §§3–4.3)。実際の境界については契約例を参照してください。
JavaScriptでは、プロセス終了コード、テストランナーステータス、またはクリーンなコンソールはそのような観測です。その意味は、有効なモード、インストールされたリスナー、ランナー設定、ビルドに依存します。uncaughtExceptionハンドラがインストールされている場合、Nodeのプロセスは「0で終了します」が、ハンドラがprocess.exitCodeを設定しない限りそうなります(Node process, uncaughtException)。Node、テストランナー、React、PlaywrightのチャネルについてはJavaScript観測チャネルを参照してください。
観測を疑わしい動作から独立させておく
期待値または不変条件がどのように得られるかをトレースします。ターゲットとチェッカーが同じ誤った答えに同意する原因となる可能性のある共有コードや前提条件を特定します。コピーされたプロダクションアルゴリズムよりも、正当化された抽象モデル、独立して指定された不変条件、または有効な関係を優先します。第二の実装は1つの選択肢です。SQLiteのSQL Logic Testは、複数のエンジンに対してステートメントを実行し、「すべてが同じ答えを得ることを確認します」。同じエンジン内の関係も別の選択肢です。SQLiteは最適化を無効にしてスイートを再実行し、SQLancerのNoRECは最適化されたクエリを最適化されていないものと比較します(SQLite testing §2、§9、NoREC実装)。
実際に比較される情報を測定します。同じ行数は行の同一性を確立しません。健全なintegrity_checkは参照整合性を確立しません。なぜなら、それは「FOREIGN KEYエラーを見つけない」からです。有効な部分チェックは保持し、ターゲットの保証が必要とする場合にのみ補完的な観測を追加します(NoREC実装、SQLite整合性チェック)。参照、正規化、または証拠を選択する際は部分観測を参照してください。
許可されたエラーとその影響をチェックする
許可された事後状態を返却ステータスとは別に導出します。SQLiteのABORTとFAILはどちらも制約エラーを返しますが、ABORTは失敗したステートメントを元に戻すのに対し、FAILは「失敗したSQLステートメントの以前の変更を元に戻しません」。エラーのみのアサーションは誤った影響を見逃す可能性があり、包括的なロールバックアサーションは正当な動作を拒否する可能性があります(SQLite conflict policies)。
実際の約束に対する観測手段を、有効な事前条件とともに選択します。SQLiteの参照整合性チェックでは、該当する外部キー観測手段、有効な強制設定、正当なNULLセマンティクスを使用します。一般的な整合性結果を代用しないでください(SQLite foreign keys、foreign_key_check)。これらは任意のAPIのデフォルトではなく、完成された契約です。
チェックの結果と限界を保持する
評価された特性と、拒否された入力、期待されるエラー、スキップされたチェック、不十分な観測を、その違いが結論に影響する場合は常に区別します。NoRECは、どちらかのカウントが-1のセンチネル(たとえば、予期されたクエリエラー後)である場合、比較をスキップし(それを等価としてカウントせず)、予期しないエラーを失敗として報告します。Elleの完全性は記録された情報に依存し、「観測が完全であることはめったにありません」(NoREC実装、Elle §4.3)。
harness-sensitivityを使用して、観測が代表的な独立して正当化された違反に到達し、それを拒否することを確立します。evidence-based-triageのために生の証拠を保持します。Elle自身のドキュメントは、「報告された異常を手動でチェックする」ことを推奨しており、ラベルを最終的な権威として扱わないようにしています(Elle README)。一般的な探索割り当てはbugfinding-campaignに属します。
選択された専門家の推論を、semantic-differential-testing、metamorphic-testing、linearizability-checking、transactional-history-testing、numerical-oracles、resource-complexity-testing、またはliveness-testingにルーティングします。このスキルが契約から観測への決定を担当します。誤解を招く近道についてはよくある間違いを参照してください。
使用可能なオラクルを返す
プロデューサー、引用された保証、有効な事前条件、実行可能な観測、結果の解釈を、具体例による許可/禁止の区別とともに返します。何が観測不可能であり、どの証拠が再生のために残らなければならないかを明記します。目撃された矛盾は、実際にチェックされた保証と前提条件のみをサポートします(Elle §§4.3 and 9)。