非決定性写像の圏におけるホーア式のモデル いちおう完結・編 - 檜山正幸のキマイラ飼育記 にて：
実行ログとは、それぞれのエクスペクテーション実行により得られた事後状態s'、戻り値y、成功・失敗の別rの組(s', y, r)を並べたものです。（注：実際には、状態を完全に記録するのは困難です。ここは概念的な話です。）
...[snip]...
実用の観点からは、実行ログが最も重要な成果物となります。
この点を少し補足：
エクスペクテーションの実行結果は、後でレポートする必要があるので、エクスペクテーションのステータスを分類しておきます。FITに倣い、ステータスを色で表示するつもりなので、色（の候補）も書いておきます。ただし、色を使うのはアクセシビリティ（色覚異常への配慮）の問題があるので、スタイルシートなどで調整可能にする必要があるでしょう。
| 番号 | 記号定数 | 意味 | 色 | |
|---|---|---|---|---|
| 1 | NotYet | 実行してない | 白 | |
| 2 | OK | 成功した | 緑 | |
| 3 | NGPreCond | 事前条件として失敗した | ピンク | |
| 4 | NG | 実行部／事後条件として失敗した | 赤 | |
| 5 | Inval | 事後条件をパスしなかった | オレンジ | |
| 6 | OKAfterNG | 失敗の後の成功 | 青 | |
| 7 | NGAfterNG | 失敗の後の失敗 | マゼンタ | |
| 8 | Error | エラー | グレー |
- 事前条件の失敗は、テストとしては成功なので、赤ではなくてピンクがいいかと。
- 強制実行をすると、失敗の後の成功／失敗が生じます。一度失敗が起きると、その後の結果は信頼できないので色を変えました。
- Invalは、それ自体は成功しても、事後条件の失敗から「正しくない」と判断されたことです。
- Errorは、綴りが間違っているとか、文字列リテラルの引用符が閉じてないとか、人間のミスの指摘です。
基本ホーアテストが成功した場合の色は、次のどちらかです。
- 緑とピンクと白の3色 -- 事前条件で失敗、テストは成功
- 全部緑 -- 事前条件が成功、実行が成功、事後条件も成功
