问题标签 [post-conditions]

在这个函数中：

后置条件不会执行（或者至少不会导致断言错误）。我现在知道它应该是：

事实上，这确实可以正常工作。

问题是这无声无息地失败了，我花了一段时间才弄清楚出了什么问题。没有语法错误，运行时异常。

我想了解 Clojure 对这段代码做了什么，以了解为什么 Clojure 没有抱怨。 宏扩展？解构？如果没有看到方括号，代码会消失吗？

我想知道是否有人可以帮助我回答这个问题。它来自以前的试卷，我可以知道为今年考试准备的答案。

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？

考虑以下涉及整数变量的代码部分：

通过陈述一个合适的输出条件，然后验证这段代码的正确性，证明执行后m等于i和j的最小值。

我的后置条件为：{m = i ∧ i < j ∨ m = j ∧ j < i}

它是否正确？你如何验证这一点？

类方法的 JML 后置条件是否可以包含对另一个方法调用的调用

例如我有这个类：

对于 doB 的后置条件，我可以有：ensures doA(x) = doA(y)？

我对这种Design by Contract方法很感兴趣。似乎preconditions必须使用已检查的异常来强制执行它们。
但是对于post-conditions和class-invariants我认为这assertions是首选。
我对吗？如果我是正确的，为什么允许 forpost-conditions和class-invariants可能被禁用的断言？不应该强制执行后置条件和不变量吗？

下面提供了 gcd 方法的前置条件和后置条件。

但是，我在遵循后置条件时遇到了麻烦......对我来说，它基本上说找到任何可以被两者整除的整数。它如何获得最大除数，实际条件是什么？

我正在尝试编写前置条件和后置条件来找到集合“col”的最大值。我不确定如何递归，所以我想知道是否有人可以提供帮助！

尊敬的专家和爱好者，

我想解决以下问题：我有一个自然数数组。我想找到他们的最大值。

但我必须用结构图展示我的解决方案，比如 http://www.testech-elect.com/pls/images/casetool2.jpg

我必须通过 midifieing 求和算法来做到这一点，这意味着我必须修改http://cfhay.inf.elte.hu/~hurrycane/programozas/programming_theorems.pdf的结构图和后置条件

必须保留主要水平线，但您可以修改其他所有内容。你能告诉我没有递归的修改后的条件吗？就够了。如果我得到它，我可以制作结构图。先感谢您。

我遇到了一个问题，提出了后置条件并显示了这段代码的部分正确性。

我不是在寻找答案，因为这是学校的作业，只是洞察力，也许是一些指向正确方向的东西。我已经构建了值表，并且无法提出循环不变量。

我知道循环的结果是 m 后面的完美正方形，但我不确定如何写。

一如既往，感谢所有帮助。

公共方法的前置条件和后置条件构成了该方法与其客户端之间的契约。

1.根据，调用者不应该验证后置条件，被调用方法不应该验证前置条件：

让我们回忆一下平方根函数 sqrt 的前置条件和后置条件，如程序 49.2 所示。调用 sqrt 的函数负责将非负数传递给函数。如果传递了一个负数，平方根函数根本不应该做任何事情来处理它。另一方面，如果将非负数传递给 sqrt，则 sqrt 有责任提供满足后置条件的结果。因此， sqrt 的调用者根本不应该检查或纠正结果。

如果操作的前置条件失败，则归咎于调用者 如果操作的后置条件失败，则归咎于被调用的操作

但正如在另一篇文章中包含的代码中所见，被调用的方法确实验证了先决条件：

a）既然满足方法的先决条件是客户的责任，那么被调用的方法是否也应该 检查先决条件是否得到满足？

b) 由于被调用方法有责任交付满足后置条件的结果，调用者是否应该检查后置条件？

2.第一篇文章中提到的一个好处是“前置条件和后置条件可用于在OOP中划分类之间的责任”，我理解这也是说验证前置条件不是被调用方法的责任，它调用者不负责验证postcondition。

但是坚持这样的理念不会使我们的代码更容易受到攻击，因为它盲目地相信对方（对方是调用者或方法）会兑现它的承诺吗？

3.如果调用者/被调用方法不盲目信任对方，那么我们不要失去很多后置条件和前置条件提供的好处，因为现在被调用方法必须承担检查前置条件的责任，调用方必须承担责任验证后置条件？

谢谢

编辑

3.

如果调用者/被调用方法不盲目信任对方，那么我们不要失去很多后置条件和前置条件提供的好处，因为现在被调用方法必须承担检查前置条件的责任，调用方必须承担验证的责任后置条件？

调用者不需要验证后置条件，因为它们应该由被调用的方法来确保。被调用的方法确实需要验证先决条件，因为没有其他方法可以强制执行合同。

a）您是否假设后置条件只应声明/保证返回值是指定类型或null（如果 返回值可以为空）？除了返回值的类型之外，后置条件还不能说明其他事情（无法通过类型系统验证），例如返回值是否在指定范围内（例如：不能后置条件也说明返回值的类型int将在 ) 的范围内10-20？在这种情况下，客户是否还需要检查后置条件？

b）那么我们可以说第一篇文章声称被调用的方法不应该检查先决条件是错误的吗？

2. 编辑

不，后置条件可以是任何东西，而不仅仅是空检查。无论哪种方式，客户端都可以假设后置条件已经过验证，例如，如果合同声明它已被确保，您不需要验证 int 范围。

a) 您之前说过，为了使代码不那么容易受到攻击，需要通过调用方法检查前置条件，但我们是否也不能推断调用方需要验证后置条件（例如，验证返回值是否在后置条件承诺的范围内）为了使调用者的代码不那么容易受到攻击？int

b）如果客户可以盲目地信任后置条件的声明（我会说当后置条件提出返回值在某个范围内的声明时，这是一种盲目信任），为什么被调用方法也不能相信调用者会满足被调用方法的先决条件？

关联

您可以将类不变量视为健康标准，操作之间的所有对象都必须满足该标准。作为类的每个公共操作的先决条件，因此可以假设类不变量成立。此外，它可以假定为类不变量所具有的每个公共操作的后置条件。从这个意义上说，类不变量作为类中公共操作的前置条件和后置条件的一般强化。有效的前提条件是与类不变量一起制定的前提条件。类似地，有效的后置条件是与类不变量一起制定的后置条件。

1.如果类上定义了类不变量Server：

a)前提条件通常是根据被调用操作的形式参数制定的，那么类不变量如何加强方法的 ( Foo')前提条件？

b)后置条件是根据被调用方法的返回值制定的，那么类不变量如何加强方法的Foo后置条件呢？

2.在类上定义的类不变量能否Caller以任何方式加强Foo的前置条件或后置条件？

3.如果在's参数上定义了类不变量：FoocmdIn

a) 如果在 range 内的状态的前提条件，但是在应该在 range 内的状态上定义的类不变量之一，那么前提条件确实得到了加强？FoocmdIn.Length1-20InputInput.Length2-19Foo

b) a ) 中的逻辑不是有点缺陷吗，因为如果类不变量已经声明Input.Length应该在范围内2-19，那么Foo定义一个并不总是存在的前提条件true不是错误（cmdIn.Length不能保存值1或20）

c) 但是如果在应该在 range 内的状态上定义类不变量，那么' 的前提条件不是加强吗？InputInput.Length0-100Foo

d)定义的类不变量cmdIn也能以某种方式加强后置条件吗？Foo

4.如果在返回值上定义了类不变量Foo

a）如果在 range 内的状态的后置条件，但是在应该在 range 内的状态上定义的类不变量之一，那么的后置条件确实是加强的？FoocmdOut.Length1-20OutputOutput.Length2-19Foo

b）但是如果在应该在 range 内的Output状态上定义不变量，那么' 的后置条件不是加强的吗？Output.Length0-100Foo

c)定义的类不变量Output也能以某种方式加强Foo的前提条件吗？

( _ _ _ _ _ Foo_还是强化Foo的前置条件和后置条件？如果这就是文章的实际含义，那怎么可能？

谢谢