问题标签 [post-conditions]

以下两个 OCL 语句对于某些函数上下文是否等效？

post: if a > 0 then b < c

post: b < c implies a > 0

我一直在阅读按合同设计的主题，到目前为止，我写了以下注释：

我想确认一个例子来澄清我的理解。

契约式设计说如果 in 的前置条件是“必须大于 10”，后置条件是“返回值在 20 到 50 之间”，那么' 方法的前置条件必须相同或更弱，并且后置条件将相同或更强。processIntexampleAexampleIntexampleBexampleInt

这意味着exampleB可能的有效前提条件是，

• 大于 0
• 大于或等于 0
• 大于 -100

但无效的先决条件是，

• 大于 20
• 在 20 到 500 范围内

同样，有效的后置条件可能是，

• 25 至 45 岁之间
• 30 到 40 之间

但无效的后置条件是，

• 20 到 90 之间
• 0 到 50 之间
• 大于 0

这是对合同设计的正确解释吗？另外，我正在用 Java 学习这个，但我认为这个概念适用于任何带有 OOP 的语言？

我正在为我的 Dafny 考试而学习，但我不知道我的代码有什么问题。

我认为这与我的“索引超出范围”错误有关，但我不知道如何解决。

任何提示将不胜感激。

问题：

我的做法：

辅助方法：

产生的错误：

在上次考试中，我有问题，我无法理智地回答。

问题是“前提条件太弱可能会出现什么问题？ ”

另一个问题是“后置条件太强会导致什么问题？ ”

如何回答这个问题？我试图解释弱前置条件评估为真，可能不足以暗示强后置条件为真，但似乎还不够。

我想知道，什么是正式的理智答案，实际上是两个简短的问题。

“前置条件弱会出现什么问题？” “强后置条件会带来什么问题？”