在我学习计算机科学的过程中，我遇到了所谓的Hoare逻辑。它的主要思想是，对于每个命令/程序，您可以定义前提条件和后置条件。这些是逻辑表达式。在启动程序之前必须满足前提条件。主要是检查所有输入是否在正确的范围内等等。它当然也可以是恒定的，这意味着：这个程序没有特定的前提条件。运行程序后必须满足后置条件。就像你的前提条件是x> 0一样，你的程序除了y：= x之外什么都不做，那么你的post条件将是：x> 0和x = y。使用一些预定义规则，您可以使用逻辑方法证明您的程序是否正确。在简单程序的情况下它很容易，但是在程序复杂的情况下它会变得非常复杂，这就是以这种方式验证程序代码真的不典型的原因。无论如何，它是一种静态代码验证方法。
所以我学会了它，通过了我的考试并忘记了这一点。
多年后，我读到了所谓的SOLID原则，还有一个名为Liskov替代原则。我的学习有一个闪回：“嗯，我已经在某个地方听到了它”。该原则如下：“如果S是T的子类型，则程序中类型T的对象可以用类型S的对象替换而不改变该程序的任何所需属性”。很明显，但事实上它意味着什么？它意味着以下内容：
- 子类型不能强化前提条件。
- 后置条件不能在子类型中被削弱。
- 超类型的不变量必须保留在子类型中
嗯，这听起来像Hoare逻辑，听起来像是有用的东西。在这一点上，我通过合同阅读了更多关于Design的内容，我在那里学到的东西让我更好地理解了如何在OOP中实现我的程序。
我想向您展示主要概念。
一个类的合同
我们可以谈谈三种不同类型的合同：不变量，前置条件和后置条件。不变属于一类，前后条件属于一种方法。
不变量只不过是对你l类状态的限制。类的状态基本上是类变量的值。例如，如果您有一个直角三角形的类，您的类变量可以是：a边的长度，b边的长度和c边的长度。这些变量及其当前值表示您的类的状态。我们知道规则：a * a + b * b = c * c，如果是直角三角形。这意味着如果我们的类代表直角三角形，那些不满足这个条件的值都是无效的，它们不代表直角三角形。所以这个逻辑表达式（a * a + b * b = c * c）可以是你的类不变量。在所有情况下都应如此。它将被检查：在构造函数的末尾，在启动任何类方法和类方法结束时。接下来是一个很好的做法，让你的类变量保持私有并通过setter和getter函数访问它们，这样你的类就永远不会得到一个无法满足不变量的无效状态。
方法的前提条件是在启动方法之前检查的条件。例如，如果您的三角形的拉伸函数具有一个名为factor的参数，则前提条件可以是此参数大于0。
一种方法的后验证。在函数结束时检查，它描述了您对方法的期望。如果拉伸函数in可能类似：a = old（a）* factor和b = old（b）* factor和c = old（c）* factor，其中old表示方法开头的值。在这里，您需要考虑class的整体状态也很重要。因此，如果它具有不应该由方法更改的属性，则它也应该在post条件中指定。例如，如果您的表示还具有颜色属性，则应使用以下颜色扩展帖子条件：color = old（color）。
到目前为止，它很简单：每个方法都有一个前置条件和一个后置条件，并且该类具有一个不变量，在构造之后以及每个函数的开始和结束时进行检查。
子类合同
如果你的类有基类，它会如何改变？
您的类保持其所有基类的不变量。因此，在一个基类的情况下，需要始终满足以下要求：invariant_of_base_class和invariant_of_your_class。
因此，从子类中，您无法打破基类的不变量。
例如，如果直角三角形类是从三角形类派生的，则三角形类的不变量可以是：a + b> = c（两个短边的长度之和应至少为最长的长度侧）。这种不变量也应该通过直角三角形来实现。
关于前后条件：
对于重写函数，前提条件不能作为基类中的前提条件加强。因此它可以减少强度（比如（a <10和b <10）只是（a <10））或与基类相同。
对于重写函数，后置条件不能作为基类中的后置条件被削弱。所以它可以是相同或更多的力量。
这被称为Liskov替代原则，它是SOLID原则的一部分。
也许它第一次有点复杂，但它没有说明：你的子类是你的基类的一个特例，所以它应该适用于所有使用基类的输入，它应该产生相同的结果同样。
在编程语言中支持合同设计
对代码使用合同设计是一种防御性编程方法，如果违反任何合同（不变量，前提条件或后置条件），程序将会出现运行时错误。通常情况下，合同检查仅在代码的测试版本中激活，并在发布版本中停用。
有一些编程语言，比如Eiffel，它们以本机方式支持合同，但它们现在并不是很受欢迎。对于当今流行的OOP语言（C ++，C＃，Java等），您可以自己实现，也不会太复杂或重用已有的库。对于C ++ Boost.Contract是一个不错的选择。对于Java，有几种开源解决方案，如Oval或Contract for Java。对于C＃，您可以使用代码合同。对于Python PyContracts。
总结
当然我知道按合同设计并不是一种常用的编程方式，我认为这是完全可以的。另一方面，在我看来，这是一种快速简便的方法来提高代码质量，让自己更多地思考“我的代码实际上在做什么”。它还使您的代码更清晰，因为您将仔细检查您的类的状态应该是什么，并且前后条件也记录了您的函数的规范。
我认为，即使您没有使用这种方法开发，也可以了解这种编程方式并考虑一下您的不变量，前后条件以及实现类以获得更好的代码质量。
(banq注：DDD聚合根实体的设计按这种合同设计)