后置条件

在计算机编程中，后置条件是一个条件或谓词，它必须在代码的某些部分执行后或在正式规范的操作后始终为真。后置条件有时在代码本身中使用断言进行测试。通常情况下，后置条件被简单地包含在受影响的代码部分的文档中。比如说。阶乘的结果总是一个整数，并且大于或等于1。所以一个计算输入数字的阶乘的程序将有后置条件，即计算后的结果是一个整数，并且大于或等于1。另一个例子：一个计算输入数的平方根的程序可能有后置条件，即结果是一个数字，其平方等于输入数。

在一些软件设计方法中，后置条件与前置条件和类不变式一起，是软件构造方法中契约设计的组成部分。任何例程的后置条件都是在例程执行完成后被保证的属性声明。由于它与例程的契约有关，后置条件向潜在的调用者提供保证，即在例程被调用的状态下，其前提条件成立，后置条件所声明的属性得到保证。

下面这个用Eiffel编写的例子根据调用者提供的参数a_hour来设置类属性hour的值。后置条件在关键字ensure之后。在这个例子中，后置条件保证在前提条件成立的情况下（即当a_hour代表一天中的一个有效小时），在执行set_hour后，类属性hour的值与a_hour相同。标签hour_set:描述了这个后置条件子句，并在运行时违反后置条件的情况下用来识别它。set_hour(a_hour:INTEGER)--设置"hour"为"a_hour"，要求valid_argument。0<=a_houranda_hour<=23dohour:=a_hourensurehour_set:hour=a_hourend

在存在继承的情况下，被子类（子类）继承的例程在其契约，也就是其前置条件和后置条件生效的情况下进行继承。这意味着任何继承的例程的实现或重新定义也必须按照其继承的契约来编写。后置条件可以在重新定义的例程中被修改，但它们只能被加强。也就是说，重新定义的例程可以增加它提供给客户的好处，但不能减少这些好处。