内容简介:在我学习计算机科学的过程中,我遇到了所谓的Hoare逻辑。它的主要思想是,对于每个命令/程序,您可以定义前提条件和后置条件。这些是逻辑表达式。在启动程序之前必须满足前提条件。主要是检查所有输入是否在正确的范围内等等。它当然也可以是恒定的,这意味着:这个程序没有特定的前提条件。运行程序后必须满足后置条件。就像你的前提条件是x> 0一样,你的程序除了y:= x之外什么都不做,那么你的post条件将是:x> 0和x = y。使用一些预定义规则,您可以使用逻辑方法证明您的程序是否正确。在简单程序的情况下它很容易,但
在我学习计算机科学的过程中,我遇到了所谓的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聚合根实体的设计按这种合同设计)
以上就是本文的全部内容,希望对大家的学习有所帮助,也希望大家多多支持 码农网
猜你喜欢:- Bing 希望改变搜索引擎发现新内容的方式
- 你了解HTTPS,但你可能不了解X.509
- 你真的了解Mybatis的${}和#{}吗?是否了解应用场景?
- 你所了解的 array_diff_uassoc 真的是你了解的那样吗?
- 图文了解 Kubernetes
- 深入了解 JSONP
本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们。
The Creative Curve
Allen Gannett / Knopf Doubleday Publishing Group / 2018-6-12
Big data entrepreneur Allen Gannett overturns the mythology around creative genius, and reveals the science and secrets behind achieving breakout commercial success in any field. We have been s......一起来看看 《The Creative Curve》 这本书的介绍吧!