问题标签 [post-conditions]

我有一个任务要求我在构造函数中创建一个空链表key: LINKED_LIST [KEY]、另一个链表data_items_1: LINKED_LIST [DATA1]和一个哈希表data_items_2: HASH_TABLE [DATA2, KEY]。我的教授提出的岗位条件是

当我运行该程序时，我违反了合同。在调试器中它总是指向这行代码，我不知道为什么。这个后置条件的目的是什么，我如何不违反本合同？

我正在为一个将棒球运行初始化为 0 的类编写一些简单的代码。它唯一的方法应该将运行次数作为其参数，并根据输入是否大于类变量返回一个布尔值和一个 int，并且 2 个中较高的一个运行如下：

我注释掉了第三个确保块，因为这是我在后置条件下的第一次刺，但它返回一个后置条件（else 块）不成立的错误，所以我选择了前两个确保（不确定它是否正确但全班验证无误）。

无论如何，当我从 main 调用 moreRuns() 时，我遇到的问题就出现了。我对返回的 bool 和 int 的断言似乎并不成立。有谁知道我哪里出错了？是我的后置条件还是我在调用 moreRuns() 之前忘记添加一些断言，还是我没有满足 val == 运行的选项？

任何提示将非常感谢！

我正在尝试在 ada 中学习自己的前后条件。

有没有办法为前置条件和后置条件指定自定义错误/失败消息，类似于Predicate_Failure谓词？我似乎无法在官方文档中找到任何内容。TIA。

我将随机进行 3 个问题的有趣测验，并提供 3 次猜测的机会。

在我尝试执行后，我尝试了正确的答案，但一直循环并告诉我的答案不正确并且无法停止循环，我不知道为什么......

谁能帮我看看？

我一直在用 c 语言编写一些基本程序，以使用 frama-c 工具进行验证。我想知道为什么断言没有在程序中得到证明。提前致谢。

所有预定目标均已成功证明，但断言声明除外：

上面的断言超时了。函数合约应该有什么修改吗？

让我思考的问题：

当我们谈到方法中的前提条件时，我们指的是由方法本身验证的条件（1）还是调用者验证的条件（2）？例如

后置条件也一样？

我有一个用数据填充的可变对象。一旦所有强制数据都存在，就可以“提交”对象。尝试提交不完整的对象会引发异常。这是一个玩具示例，其中一个对象的content初始值为None, 并且必须在提交之前填充一个字符串。

这段代码的结构不是很好：应该有一个单独的方法来检查完整性。（在我的真实代码中，该方法会在多个地方被调用，因为有几种不同的“提交”方式。）

我使用 mypy 0.780 来检查类型。可以理解的是，它抱怨上面的代码：

这很公平：在第一个“内联”版本中，mypy 足够聪明，可以知道它self.content具有类型str，因为它具有类型Optional[str]，并且这部分代码只有在self.content is None为 false 时才可访问。在具有check_completeness单独方法的版本中，mypy 不会推断该方法的后置条件是 that self.contentis not None。

如何让 mypy 知道check_completenessis self.content is not Noneor的后置条件self.content : str？为了保留完整性检查的封装（在我的真实代码中要大得多），我不想重复里面的条件commit。我宁愿保持commit上述第二个版本不变。我可以满足于重复：

但这无济于事：mypy 不会扩展方法调用来推断调用的后置条件assert。

我一直在尝试很多事情并寻找解决方案，但我找不到。

我被卡住了，因为我需要为 ada 函数中的后置条件分配一个新值

例如，使用以下函数：

我想知道如何例如增加参数 A 或将其设置为后置条件内的随机值，如 42

谢谢

我有一个编程语言的函数，例如 C。我要求函数的输出满足某个条件。如果此函数的某些输入的输出不满足要求的条件，我需要找到任何这样的精确输入。

我通常需要这样做，但对于相当简单的功能，例如循环的数量是固定的并且不依赖于输入。另一个要求是我需要非常快地做到这一点。我发现 CBMC 工具 [https://www.cprover.org/cbmc/] 可能对我有帮助，但我不知道如何使用它。我也欢迎将问题转换为 CNF 公式的解决方案（但我仍然需要检索反例输入）。

函数示例：