ACM通信
运行时断言:您在等待什么?
ACM论坛上的评论comp.risks正如上一篇文章所述，为反思软件质量技术提供了一个很好的起点。
在最新一期关于风险，Henry Baker评论了David Wheeler[2]的一篇关于“如何防止下一个心脏出血”的在线文章，指的是最近发现的全球性互联网漏洞。
这两篇文章都主张使用运行时断言监视(Wheeler有一些保留意见)，而且都实现了一个了不起的壮举，即不引用Eiffel环境，在该环境中运行时断言监视已经例行地实践了几十年。使用Eiffel是否能够避免导致Heartbleed的特定错误只能推测，但对于每天使用契约设计技术(关于最近记录实际使用的论文，请参阅[3])的用户来说，这是不可猜测的:运行时断言监视可以捕捉到左右的错误。
Baker莫名其妙地反对运行时断言监视证明。他写道:
不幸的是，证明[一个)软件系统忠实地实现了该模型不可判定的在本质上每一个有趣的系统．
这意味着它是绝望的期望任何语言、编译器或类型检查系统都能先验地保证忠实对所有输入．
并进一步指出:
形式分析不能用来证明程序的正确性，
恐怕贝克先生应该重新审视一下他对不可捉摸性的理解(如果问题出在这一点上，或许可以改进一下他的评论措辞)。不可能的是设计出一种可以证明的通用机制任何contract-annotated (assertion-equipped)计划。这并不妨碍机械的证明具体的项目。许多研究人员——以及越来越多的实践者——使用证明工具对越来越雄心勃勃的程序执行机械验证，他们会惊讶地发现他们的工作是不可能的。两个现代证明工具的例子包括来自Altran Praxis的Spark，它已经证明了部署的生命关键系统的正确性，以及Microsoft Research的Boogie，它是Eiffel的自动证明环境所依赖的。
实际上，静态验证和动态断言监视是互补的。有时证明是可能的(在今天的技术中，总是在经过大量的人力努力指导证明过程之后)。有时候失败。在后一种情况下，动态断言监视是解决方案;正如贝克所写的，人们应该这样做
文档每一个带有积极运行时断言的假设。
他说得很对。这种方法是我的文章和书籍长期以来提倡的，也是埃菲尔用户所采用的。我们谈论的不仅仅是散布在代码中的断言——以C或Java“断言”或JUnit断言的风格——而是契约。不同之处在于，这些契约被复杂地编织到代码结构中，不仅作为一致性检查出现，而且作为与设计的结构元素相关的规范元素出现:例程(先决条件、后置条件)、循环(循环不变式和变量)、类(类不变式)。因此，它们是软件构建过程中不可分割的一部分，从需求到设计和文档，再到实现、维护和验证。我在写"验证“而且不仅仅是”测试“因为核查有多种形式，有些是静态的，有些是动态的。
不应该只使用偶然的断言，而应该使用集成在代码结构和软件构建过程中的契约的原因之一是软件开发中更改的重要性。当程序被更新时(这总是会发生)，很难确保开发人员总是插入新的检查并根据需要更新旧的检查。当前置条件、后置条件、类不变量和其他结构元素是软件不可分割的一部分时，就更容易执行同时更新规范和实现的规程。
在埃菲尔铁塔的主要实践中，合同大多用于动态监控(在其验证作用中)，正如贝克所建议的那样。当它们将与静态防工具常规结合的日子越来越近了;有关此类集成如何工作的示例，请参阅EVE (Eiffel验证环境)的参考资料，从[4]中的原始演示开始。
Wheeler还提到了运行时断言验证，但指出
这种方法在对抗心脏出血时确实有一些弱点。最初的开发人员和审核人员都没有意识到检查请求包长度值是重要的;由于长度检查没有包括在内，开发人员不太可能记得添加断言来检查它。
在这里，普通运行时检查和契约之间的区别也是至关重要的。当人们没有真正实践契约式设计时，他们会错过的是，我们不只是进行一些零星的健全检查。我们使程序员能够根据明确说明的规范开发他们的设计和代码。这种方法经常导致发现一些假设，如在Heartbleed案例中，这些假设对于程序的正确性是至关重要的，但有被忽略的风险。
然后我们加强这些假设;例如,动态。
参考文献
[1]亨利·贝克:心脏出血和正式方法,在风险论坛27.89, 2014年5月7日，彼得·g·诺伊曼主编，可用在这里．
[2]大卫·惠勒:如何防止下一次心脏出血， 2014年5月11日修订，已出版在这里．
h - christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni和Bertrand Meyer:合同在实践中(本周)出现在FM 2014第19届形式方法国际研讨会论文集，新加坡，2014年5月，草案可用在这里．
[4] Julian Tschannen, Carlo A. Furia, Martin Nordio和Bertrand Meyer:结合静态与动态技术的面向对象程序可用性验证,在SEFM 2011，软件工程与形式化方法，蒙得维的亚，2011年11月14-18日，计算机科学课堂讲稿，施普林格Verlag, 2011，已有版本在这里．
评论
迈克·汉德里
迈耶先生，谢谢你的帖子。我同意你对贝克先生的评论的解释，但原因不同。事实上，我希望像您这样的作者能更好地阐述这个问题。
如果软件构建本身可以被认为是一个巨大的状态机，有大量但有限的预期状态，我们仍然不能称它为图灵机。它不一定有有限数量的输入(这也包括模块接口)。因此，我们无法知道任何有状态分支是否会如预期的那样终止。从本质上讲，贝克试图将检查系统的分析简化为停止问题:他说得有点对，我们无法知道它的行为，但因为在前端或模块化接口之间有大量未规划的输入，这不仅是因为决定论的失败。Heartbleed是最糟糕的情况，到达一个可接受的状态，但这是因为没有为该状态机定义输入。
合同的论点是减少这些计划外/带外输入的风险，这样软件构建确实更像图灵机，具有可预测的结果。契约不能解决模块化接口的语义阻抗不匹配问题，但它可以为解决这个问题提供一个正式的过程。它肯定可以治愈错误的输入，使您的构建变成一个不像大型(模态)图灵机的东西。如果把这个建筑说成是一个管道装置，合同会确保接头焊接到一定的标准，特别是因为错综复杂的饮用水管道最终会淹没在毒药中，它更多的是毒药进入而不是水流出。合同不能保证你把热水和冷水送到你想要的地方。
显示1评论