问题标签 [post-conditions]

I try to use across 1|..|list.count as j all list.i_th(z) ~ old list.i_th(z) end

but it says unknown identifier z. Whats wrong with this syntax??

我正在阅读有关使用关键字验证方法前置条件和后置条件的Oracle 文档。assert

该文档说可以使用assert关键字来验证public方法的后置条件，但您应该只使用assert关键字来验证private方法的前置条件。

为什么是这样？

在 Programming: Principles and Practice using C++ 的第 5.10.1 章中，有一个“Try this”练习用于调试某个区域的错误输入。前置条件是长度和宽度的输入是否为 0 或负数，而后置条件是检查面积是否为 0 或负数。引用这个问题，“找到一对值，使这个版本的区域的前置条件成立，但后置条件不成立。”。到目前为止的代码是：

虽然代码似乎可以工作，但我无法理解哪些输入将使前置条件成功但会触发后置条件。到目前为止，我已经尝试在其中一个输入中输入字符串，但这只是终止程序并尝试查找等同于 0 的 ascii，但结果也相同。这应该是某种技巧问题还是我错过了什么？

我正在使用 EA 对一些 c 组件进行建模。我知道 EA 不能有效地与 C 语言一起使用，但我试图尽可能地坚持每个元素的预期用途。

我的问题...我正在使用一个类和使用此类中的操作的函数对 C 文件进行建模。我的函数需要在它们开始之前接收一些值并在它们完成之前发送一些其他值，我可以使用操作的 Pre 和 Post-Coditions 在模型中表示这个还是不适合这个地方？如果不是，我应该如何以正确的方式在模型中表示这一点

所以我是 Eiffel 编程的新手，我正在尝试学习在ensurea 的块中编写后置条件feature，特别是编写循环。

所以我尝试了这个：

但由于某种原因，我得到了一个未知标识符iand j。有谁知道导致此错误的原因以及我该如何解决？across ... as ... all ... end另外，在ensure块中使用还有另一种选择吗？提前非常感谢！

我的老师告诉我以下语句是有效的： {x > 3} while true (x := 3) {x = 3}

为什么这个说法有效？是因为后置条件永远不会被检查，还是后置条件现在算作不变检查？

简而言之：当存在无限循环时，后置条件可以是任何东西吗？

那么这将是有效的： {x > 3} while true (x := 3) {x = 0}

我可以理解这段代码中前置条件的含义和目的，但我在理解后置条件的含义和目的方面存在问题。在Push我知道这部分在推整数后增加指针（指针=指针~+1）。在Pop我理解这部分是在弹出整数后减少指针（Pointer=Pointer~ - 1）。

我想知道是否有任何工具可以根据方法的前置条件和后置条件（以及类不变量）自动生成单元测试。

准确地说，假设我们给定了方法的前置条件和后置条件（可能还有类不变量），并且我们希望基于该信息生成单元测试。为此，我正在寻找一种实用的工具。

我知道 Korat 和 TestWizard。您能否再列举一些技术/工具？

PS：编程语言，或者我们指定方法契约使用的语言，并不那么重要。我只是想了解技术。

谢谢你。

我试图证明一种方法的正确性，该方法确定大小序列是否n是. 我设法证明，只要方法返回，那么序列确实是有效的排列。尽管如此，证明相反的情况要困难得多（对我来说）。我认为我有正确的循环不变量和触发器，但是 Dafny 触发了一个我无法理解的断言错误。这是永久链接，这是完整的代码：0,1,...,n-1true

我有一种方法可以将数组中的所有项目向左移动一个位置。在我的后期条件下，我需要确保我的物品已经向左移动了一个。我已经将旧数组的第一个元素与新数组的最后一个元素进行了比较。我如何遍历从 2 到 count 的旧数组，从 1 到 count-1 循环遍历新数组并比较它们？这是我到目前为止的实现。

我希望结果是正确的，但我得到了指向这个后置条件的合同违规。我已经通过在方法之前和之后打印出数组来手动测试该方法，我得到了预期的结果。