先决条件

在计算机编程中，先决条件或先验条件指在执行一段代码前必须成立的条件。

简介如果先决条件被违反了，则代码将产生未定义行为，因此其预期的工作能否履行也是未知的。不正确的先决条件还可能引发安全问题。

通常，先决条件包括在关于这段代码的文档中。有时它可通过特定的语法结构（如警卫或断言）在代码中进行检测。

例如，阶乘只定义于自然数（大于等于零的整数）。因此计算阶乘的程序将会假定输入的值是一个整数，并且它大于等于零，这就是一个先决条件。1

在面向对象编程中面向对象编程中先决条件是契约式设计的一个重要组成部分。契约式设计还包括后置条件和不变条件的概念。

要成功执行一个子程序所需的任何关于对象状态的限制条件都定义在先决条件中。从程序开发者的角度来看，这就构成了契约中子程序调用者的一部分。调用者有义务来确保在调用子程序前满足先决条件，而被调用的子程序则以后置条件来反馈给调用者。1

先决条件与继承在继承的关系中，继承了子程序的子类必须满足先决条件。也就是说对被继承的子程序的任何实现或重新定义，也必须遵守他们所继承的契约。重新定义的子程序可以削弱先决条件，但不能增强。1

不变条件在计算机科学中，不变条件是指，在程序执行过程或部分过程中，可始终被假定成立的条件。比如，循环不变条件是指在循环开始和结束后始终成立的条件。

不变条件在逻辑推理计算机程序正确性时，特别有用。优化编译器理论、契约式设计设计方法论及形式方法，都十分依赖于计算机程序的不变条件。

程序员往往使用断言来现式定义不变条件。一些面向对象编程语言也有特定语法定义类不变条件。1

契约式设计契约式设计（英语：Design by Contract，缩写为 DbC），一种设计计算机软件的方法。这种方法要求软件设计者为软件组件定义正式的，精确的并且可验证的接口，这样，为传统的抽象数据类型又增加了先验条件、后验条件和不变式。这种方法的名字里用到的“契约”或者说“契约”是一种比喻，因为它和商业契约的情况有点类似。

因为Design by Contract是属于Eiffel Software的注册商标，很多开发人员用契约式编程（Programming by Contract），契约编程（Contract Programming），或者契约优先式开发（Contract-First development）来指代这种方法。微软也采用这种设计方法，称为代码合约（Code Contracts）。2

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所