计算机术语中的前置条件,后置条件和不变量有何不同

Question

我正在阅读Java Concurrency in Practice这本书,并对这些术语感到困惑:

1. 预先条件
2. 发布条件
3. 不变

有人可以解释一下他们(举个例子,如果可能的话)？

Answer 1

如果您无法理解这些简单的想法,那么编写Java会遇到很多问题,特别是多线程代码:

1. 前置条件是在调用方法之前必须为真的事物.该方法告诉客户"这是我对你的期望".
2. 后置条件是方法完成后必须为真的事情.该方法告诉客户"这是我保证会为你做的".
3. 不变量是永远正确且不会改变的事物.该方法告诉客户"如果在你打电话给我之前这是真的,我保证当我完成时它仍然是真的".

它们都是"合同编程"这一概念的一部分.它是由一个名叫CAR Hoare的人发明的.Bertrand Meyer 围绕它构建了一个名为Eiffel的面向对象语言.没有人使用它,但他因此而在阳光下度过了一天.

埃菲尔不是很受欢迎.在我写这篇文章时,有超过四百万个问题,但只有32个被标记为"埃菲尔".

更新:2016年6月29日,SO上有11,966,392个问题.其中只有92个被标记为"埃菲尔".埃菲尔问题的百分比大致保持在~0.00077%.

我的立场得到了纠正 - 谢谢你,flamingpenguin.我已经更新了我的答案.