4種類の使い方
- 正しいソフトウェアを書くのを手助けする
- 文書化の支援
- テスト・デバッグ・品質保証をサポートする
- 耐障害性をサポートする
- おそらく最も重要
- (実装に依らない)形式的な性質を厳密に記述する
- クラスのソースから、実装部分を省略した形式
- 表明はショート形式に残る
特徴
- HTMLやRTF等様々な形式に変換可能
- ソースに記述する
- クラスから抽出可能
- Java等のインタフェースと違って二度書く必要がない
設計の検討等の際に、(実装よりも?)ショート形式が中心に使われる
表明を実行時にチェックする(そして例外を投げる?)事が可能
表明の実行時チェック方法
- コンパイルオプションで指定する
- Ace ファイル(Makefile みたいな物?)に記述する
- ソースを見る限りではサブモジュール単位で指定?
検査のレベル
- no, require, ensure, invariant, loop, check
- それぞれ、上のレベルの検査も包含する
ケースバイケース
- 開発中は全てオンにするべき
- スピードが特に求められる場合はオフ
デフォルトは事前条件のみのチェックしている
- パフォーマンスのロスが他と比べて少ない
- 信用できるライブラリの使用時等は事前条件が望ましい
例: 配列の検査
- ホーア曰く「常に行うべき」
- 製品で頻繁に起こりうるのなら行うべき
- 別の考え方
- 事前条件の違反が稼働時に頻繁に起こるなら、それは開発体制の問題
- 事前条件のチェックに依存した製品になる恐れがある
パフォーマンス
- 表明のチェック自身よりも、スタックトレース等が高コスト
適応レベルの選択基準、原則
- 製品版でチェックが有効である事を前提としない
- 開発中は最低事前条件はチェックする
- 製品版の基準
- ソフトウェアの正しさをどれだけ信用するか
- 最大の効率を得る事がどれだけ重要か
- 未発見の実行時エラーの結果はどれだけ深刻か
- チェック版も配布物に含める
実行時以外でソフトウェアが正しい事を完璧に検証する事は出来ないから
表明で記述出来ないこともある
- 代わりにコメントを書く事で回避する
表明の中でルーチンを呼び出しても良い
- 表明の記述力が強化される
- ただし表明の中に命令的な要素が入り込んでしまう
- ルーチンの適用的要素と命令適用その分離は行う
- 表明の中で呼び出されたファンクションの表明の評価はしない
参照先のオブジェクトが変化する事で、不変条件が壊れることがある(間接不変表明効果)
- 例あり
対策
- ルーチンの入り口と出口で検査する
- 出口だけでは間接不変表明効果かどうかを判別できないため
- ミラー句
- 単に、参照先に二重の不変条件を記載するだけの模様
略…