使用DBC,类的编写者显式地规定针对该类的契约。客户代码的编写者可以通过该契约获悉可以依赖的行为方式。
契约是通过为每个方法声明的前置条件和后置条件来指定的要使一个方法得以执行,前置条件必须要为真。执行完毕后,该方法要保证后置条件为真。
派生类的前置条件和后置条件的规则是:
在重新声明派生类中的例程时,只能使用相等或者更弱的前置条件来替换原始的前置条件,只能使用相等或者更强的后置条件来替换原始的后置条件。换句话说,当通过基类的接口使用对象时,用户只知道基类的前置条件和后置条件。因此,派生类对象不能期望这些用户遵从比基类更强的前置条件。也就是说,它们必须接受基类可以接受的一切。同时,派生类必须和基类的所有后置条件一直。也就是说,它们的行为方式和输出不能违反基类已经确立的任何限制。基类的用户不应被派生类的输出扰乱。