【问题标题】:Understanding complex post-conditions in DbC了解 DbC 中的复杂后置条件
【发布时间】:2026-01-16 09:30:01
【问题描述】:

我一直在阅读按合同设计的帖子和示例,但有些东西我似乎无法理解。在我看到的所有示例中,DbC 都用于在后置条件(例如大量银行账户)中测试其自身状态的普通类。

在我看来,大多数时候当你调用一个类的方法时,它会做更多的工作来将方法调用委托给它的外部依赖项。我了解如何在具有特定场景的单元测试中使用依赖反转和模拟对象(专注于方法的外部行为)来检查这一点,但是这如何与 DbC 和后置条件一起工作?

我的第二个问题必须处理理解复杂的后置条件。在我看来,要为许多函数写出一个后置条件,你基本上必须为你的后置条件重新编写函数体,才能知道新状态将是什么。那有什么意义呢?

我真的很喜欢 DbC 的概念,并且我认为它有很大的前景,特别是如果我能够在找到经过验证的合同后弄清楚如何重现某些失败状态。在过去的几个小时里,我一直在阅读一些简洁的东西。 Eiffel 中的自动测试生成。我目前正在尝试改进我在 C++ 开发中的流程,但如果我能弄清楚如何不失去我在当前项目中取得的所有基础,我愿意学习新的东西。谢谢。

【问题讨论】:

    标签: design-by-contract


    【解决方案1】:

    但这如何与 DbC 和 后置条件?

    每个功能基本上都是其中之一:

    • 语句序列
    • 条件语句
    • 一个循环

    这个想法是,您应该检查有关函数结果的任何后置条件,这些后置条件超出了所有被调用函数的后置条件的联合。

    你基本上必须重写 你的函数体 后置条件知道什么是新的 状态将是

    反过来想。是什么让你首先编写这个函数?你追求什么?可以用比函数体本身更简单的后置条件来表达吗?后置条件通常使用查询(在 C++ 中是 const 函数),而主体通常结合命令和查询(修改对象的方法和仅从中获取信息的方法)。

    一些的情况下,是的,你会发现你真的可以用后置条件增加一点价值。在这些情况下,编写一堆测试通常就足够了。


    另见:

    【讨论】:

      【解决方案2】:

      合同级别的委派

      大多数时候你打电话给 一个类的方法,它做的更多 工作委派方法调用其 外部依赖

      至于第一个问题:一个函数/方法的实现可能会调用很多其他的函数/方法,但是如果代码的设计者思路清晰,这并不意味着规范是被调用者规范的串联。对于调用许多其他方法的方法,如果该方法完成了精确且定义明确的任务,则规范的大小可以保持不变。如果整个系统设计良好,它应该这样做。

      您显然是从运行时断言检查的角度提出问题。在这种情况下,上述内容可能会表达为“您不需要重新检查调用者的后置条件,即所有被调用者都遵守了各自的合同。这些检查已经在每次调用时进行。在调用者的后置条件中,只检查调用者的功能上可见的结果。"

      了解复杂的后置条件

      您可能会发现这个"ACSL by example" document 很有趣(尽管可能与您习惯的不同)。它包含许多 C 函数的正式合同示例。合约的语言旨在用于静态验证而不是运行时检查,具有它所带来的所有优点和缺点。它们比你提到的“银行账户”要复杂一些——这些函数实现了真正的算法,虽然很简单。该文档通过引入经过深思熟虑的辅助 谓词(在 Eiffel 中称为 queries,正如 Daniel 在他的回答中指出的那样),使合同保持简短和可读。

      【讨论】: