契約プログラミング

出典: フリー百科事典『ウィキペディア(Wikipedia)』

これはこのページの過去の版です。TAKAHASHI Shuuji (会話 | 投稿記録) による 2020年9月6日 (日) 13:32個人設定で未設定ならUTC)時点の版 (英語版 Design by contract の翻訳によりトップの画像を追加しました。)であり、現在の版とは大きく異なる場合があります。

design by contractのスキーム

契約プログラミング(けいやくプログラミング、Programming By Contract)または契約による設計(けいやくによるせっけい、Design By Contract)とは、プログラムコードの中にプログラムが満たすべき仕様についての記述を盛り込む事で設計の安全性を高める技法。プログラミング言語Eiffelで初めて導入された。"Design by Contract" の頭文字からとった DbC (ディービーシー) でよばれることが多い。

概要

ソフトウェア開発工程で、あるコードを使用した際にエラーが生じたとする。この時エラーには2つの可能性がある:

  • コードの実装に誤りがあった
  • コードを使う側に誤りがあった。

契約では、コードの利用条件を主処理とは別に定めることでエラーの位置を明確にする。契約違反が発生すると例外などの形で実行は中断される。

これは仕様をドキュメントとして付属する代わりに、実行可能な形態でコードの一部にできるという事である。最終的な配布物はコンパイラオプションで契約用コードを取り除く。従って実行効率にも影響しない。

条件の種類

契約は、コードの利用条件が満たされることによって成立する。 それら条件は、満たすべきタイミングと主体によって、以下の3種類に分けられる。

事前条件 (precondition)
サブルーチンの開始時に、これを呼ぶ側で保証すべき性質。
事後条件 (postcondition)
サブルーチンが、終了時に保証すべき性質。
不変条件 (invariant)
クラスなどのオブジェクトがその外部に公開しているすべての操作の開始時と終了時に保証されるべき、オブジェクト毎に共通した性質。

コードを呼ぶ側が事前条件と不変条件を満たす義務を負うことで、呼ばれたコードはその条件が恒真であるとの前提を利益として得る。引き換えに、呼ばれたコードは事後条件と不変条件を義務として負い、呼ぶ側の利益としてこれを保証する。

契約をサポートする言語