如果先决条件被违反了,则代码将产生
未定义行为,因此其预期的工作能否履行也是未知的。不正确的先决条件还可能引发
安全问题。
通常,先决条件包括在关于这段代码的文档中。有时它可通过特定的语法结构(如警卫或
断言)在代码中进行检测。
例如,
阶乘只定义于自然数(大于等于零的整数)。因此计算阶乘的程序将会假定输入的值是一个整数,并且它大于等于零,这就是一个先决条件。
要成功执行一个
子程序所需的任何关于对象状态的限制条件都定义在先决条件中。从程序开发者的角度来看,这就构成了契约中子程序调用者的一部分。调用者有义务来确保在调用子程序前满足先决条件,而被调用的子程序则以
后置条件来反馈给调用者。
在继承的关系中,继承了子程序的子类必须满足先决条件。也就是说对被继承的子程序的任何实现或重新定义,也必须遵守他们所继承的契约。重新定义的子程序可以削弱先决条件,但不能增强。
不变条件在逻辑推理计算机程序正确性时,特别有用。优化编译器理论、
契约式设计设计方法论及形式方法,都十分依赖于计算机程序的不变条件。
契约式设计(英语:Design by Contract,缩写为 DbC),一种设计
计算机软件的方法。这种方法要求软件设计者为
软件组件定义正式的,精确的并且可验证的接口,这样,为传统的
抽象数据类型又增加了先验条件、后验条件和不变式。这种方法的名字里用到的“契约”或者说“契约”是一种比喻,因为它和商业契约的情况有点类似。
因为Design by Contract是属于Eiffel Software的注册商标,很多开发人员用契约式编程(Programming by Contract),契约编程(Contract Programming),或者契约优先式开发(Contract-First development)来指代这种方法。微软也采用这种设计方法,称为代码合约(Code Contracts)。