契約による設計
> 契約による設計 (DbC) は、Eiffel プログラミング言語で最初に導入され、その言語がこの概念を直接サポートしています。Python などの他の言語も DbC の要素をサポートするライブラリを持っています。DbCは型システムとは異なり、特定の関数やメソッドの前置条件、後置条件、不変性を明確に定義することを重視しています。
>
> 以下に Eiffel での契約による設計の例を示します：
eiffelclass ACCOUNT
feature -- Access
balance: INTEGER
-- Money available
feature -- Element change
deposit (sum: INTEGER) is
-- Deposit `sum'.
do
balance := balance + sum
ensure
balance = old balance + sum
end
withdraw (sum: INTEGER) is
-- Withdraw `sum'.
require
sum >= 0
sum <= balance
do
balance := balance - sum
ensure
balance = old balance - sum
end
end>この例では、ACCOUNTクラスが二つのメソッド、depositとwithdrawを持っています。depositメソッドにはensureキーワードを用いて後置条件を定義し、withdrawメソッドではrequireキーワードを用いて前置条件を定義しています。これらの条件は、メソッドが正しく機能するための契約を表現しています。
>
> 契約による設計は型システムとは異なるものですが、お互いを補完する存在です。型システムはデータの形式と操作を規定する一方、契約による設計は特定の操作が適用される条件や、操作後の状態を規定します。両者は共に、プログラムの正確性を保証するのに役立ちます。