问题标签 [post-conditions]

使用 Chromium 代码库时，我已经习惯了CHECK(condition);,DCHECK(contidtion)和NOTREACHED;. 它们向代码引入断言（通常是先决条件），并允许在日志中使用一些信息终止程序，在调试构建中DCHECK，并且NOTREACHED还会停止调试器来调查案例。第一个仅在发布模式下处于活动状态，后两个仅在调试中处于活动状态 - 当“不活动”时，它们将被空宏替换并且不会造成任何开销。

Java中是否有一些库允许这样的事情？我知道我可以根据配置交换配置创建一些静态方法/对象，但我看不到避免产生开销的方法。此外，我不想重新发明轮子。

在不违反替代原则的情况下，我很难理解前置条件和后置条件必须如何工作。所以让我们假设我们有一个类Rectangle并且——Square如何关联它们？哪一个必须是子类？

所以我理解 a 的前置条件Subtype可以更弱，这意味着我们可以在子类中取一个主要的“集合”，另一方面，后置条件可以更强，所以我们可以返回一个次要的“集合” ' 东西的。如何在我的示例中应用这些规则？

我读到基类必须比子类“做”得少，所以我认为这Square必须是我们的基类和Rectangle子类。因此， in 的前置条件Square必须是 assert that height == width，但后置条件和 in 的前置条件Rectangle呢？

我遇到的问题是两个不同类中的两种不同方法不合作，设置如下：

一个主要的称它们如下：

为什么方法d不承认方法b确保了它的前提条件？如果这是对 Dafny 证明者的限制，我将如何解决这个问题？

编辑： 当我创建这个例子时弄乱了语法，所以测试程序可以工作。然而，真正的仍然有问题。我正在努力解决的具体课程如下所述：

主要它被称为如下：

我正在学习如何编程，但我无法完全理解的一件事是 preconditions 和postconditions。

调用函数之前的 if 语句是否被视为前提条件，或者在大多数语言中是否有单独的更有效的方法？

我也在努力寻找任何我能以我目前的编程知识理解的先决条件的例子，如果有人能证明一个简单的例子，那么我真的很感激（任何语言都可以）

考虑以下接口：

假设entity、target和world都是有效的输入。但是用于查找路径的算法（在这种情况下是 Astar）无法找到路径，例如。目标被混凝土墙包围的位置。

声明后置条件是从实体到目标的路径（开始到目标）或 NoPathException（假设未找到路径）是否有效？ -或者前提条件是必须有一条从起点到终点的有效路径？

这不是作业，而是改进我们学期项目报告的问题。我不想学习任何框架，这纯粹是关于合同设计的标准和形式问题。感谢您对此事的任何澄清。

我见过的最强后置谓词转换器的每个公式都呈现如下分配规则：

我想知道，为什么上述规则中需要存在（以及存在量化的变量“v”）？在我看来，最强的后置条件谓词转换器几乎与符号评估相同，因为您维护一个状态（从变量到值的映射）和一个路径条件（一个谓词，在程序中的特定点必须为真）。然而，符号评估并不依赖于存在量词。

所以，我想我一定在这里遗漏了一些东西。任何帮助表示赞赏！

假设我有以下课程：

我Player的play()方法的前置/后置条件是什么？

我对前提条件的回答将以roundsPlayed变量为中心，

但是我想知道我的前置/后置条件是否应该包括我Board在我的方法中使用 the 和可能它的变量的事实

我的回答中是否应该考虑我的前置/后置条件Board？

在《Think Python: How to Think Like a Computer Scientist》中，作者将后置条件定义为：

函数结束前应满足的要求。

他还说：

相反，函数末尾的条件是后置条件。后置条件包括函数的预期效果（如绘制线段）和任何副作用（如移动 Turtle 或进行其他更改）。

所以假设我们有一个名为factorial的函数，它有一个名为n的必需参数，它的预期后置条件不是它必须（即它必须）返回一个表示从1到n的数字的乘积的正整数吗？阶乘结束后不满足这个要求吗？

这个定义对吗？

将后置条件定义为“函数结束后应满足的要求”。对吗？

注意：我是编程的初学者，一般来说，尤其是 Python。

基本上，如果列表中尚不存在一个元素，我希望将其添加到列表中。在方法完成后有一个后置条件来确保该元素存在于列表中似乎是合理的。下面是一个最小的例子，它给了我错误“CodeContracts：确保未经证实：_numbers.Contains(n)”。有什么想法为什么它不起作用，或者是否有办法重写代码以使其起作用？

我已经实现了一个查询，它告诉数组是否已排序。我想制作一个好的后置条件，可以有效地检查数组是否使用across或其他方式排序。

我试着这样做：

我试着写这样的东西：

但这显然行不通，因为el.forth它不是查询，而是命令。

我怎样才能使这项across工作或我应该做其他事情？