问题标签 [invariants]

我有一个在 MySQL 数据库中编码为边的树：

对于树上的每一片叶子，items.tot都是由某人设置的。对于内部节点，items.tot需要是其子节点的总和。重复运行以下查询将生成所需的结果。

（请注意，这实际上不起作用，但这不是重点）

假设数据库存在并且已经满足不变量。

问题是：

在保持此要求的同时更新数据库的最实用方法是什么？更新可能会移动节点或改变tot叶节点上的值。可以假设叶节点将保留为叶节点，内部节点将保留为内部节点，整个事物将保留为一棵适当的树。

我曾经有过的一些想法：

• 完全失效，在任何更新后，重新计算一切（嗯......不）
• 在 items 表上设置触发器以更新已更新的任何行的父级
  • 这将是递归的（更新触发更新，触发更新，...）
  • 不起作用，MySQL 无法更新启动触发器的表
• 设置触发器以安排更新任何已更新行的父级
  • 这将是迭代的（从计划中获取一个项目，处理它以安排更多项目）
  • 这是什么开始？信任客户端代码来做对吗？
  • 一个优点是，如果更新正确排序，则需要计算机计算的总和更少。但这种排序本身就是一个复杂的问题。

一个理想的解决方案将推广到其他“聚合不变量”

FWIW我知道这“有点过火”，但我这样做是为了好玩（有趣：动词，通过这样做找到不可能的事情。:-)

这个词似乎在许多情况下使用。我能想到的最好的是它们意味着一个无法改变的变量。这不是常量/finals（该死的Java！）的用途吗？

我很想听听您在操作期间使用什么技术来验证对象的内部状态，从它自己的角度来看，这些技术只会因为内部状态不好或不变的破坏而失败。

我的主要关注点是 C++，因为在 C# 中，官方和流行的方法是抛出异常，而在 C++ 中并没有唯一的方法可以做到这一点（好吧，在 C# 中也不是，我知道）。

请注意，我不是在谈论函数参数验证，而是更像是类不变完整性检查。

例如，假设我们想要一个Printer对象Queue异步打印作业。对于 的用户Printer，该操作只能成功，因为异步队列结果在另一个时间到达。因此，没有相关的错误代码可以传达给调用者。

但是对于Printer对象而言，如果内部状态不好，即类不变量被破坏，则此操作可能会失败，这基本上意味着：一个错误。该条件不一定对Printer对象的用户有任何兴趣。

就个人而言，我倾向于混合三种内部状态验证风格，我无法真正决定哪一种是最好的，如果有的话，只能确定哪一种绝对是最差的。我想听听你对这些的看法，也想听听你在这件事上分享你自己的经验和想法。

我使用的第一种风格 - 以可控的方式失败比损坏数据更好：

我使用的第二种风格 - 比损坏的数据更好的崩溃无法控制：

我使用的第三种风格 - 比损坏的数据更好地静默和防御性地纾困：

我对样式的评论：

1. 我认为我更喜欢第二种风格，其中不隐藏故障，前提是访问冲突实际上会导致崩溃。
2. 如果它不是不变量中涉及的 NULL 指针，那么我倾向于倾向于第一种样式。
3. 我真的不喜欢第三种风格，因为它会隐藏很多错误，但我知道有人更喜欢在生产代码中使用它，因为它会产生一种不会崩溃的强大软件的错觉（功能只会停止运行，如损坏Printer对象上的排队）。

您更喜欢其中的任何一个，还是有其他方法可以实现这一目标？

我不喜欢在 JPA 实体上至少有一个空的构造函数和公共设置器的要求。虽然我了解 EntityManager 方面的问题，但这会使类不变量无效。

有没有人对此有解决方案（设计模式或成语级别）？

谢谢！

伊戈尔

我试图在代码合同中演示不变量，我想我会举一个字符串排序列表的例子。它在内部维护一个数组，有用于添加等的备用空间 - 基本上就像List<T>. 当它需要添加一个项目时，它将它插入到数组中，等等。我想我有三个不变量：

• 计数必须是合理的：非负数并且最多与缓冲区大小一样大
• 缓冲区未使用部分中的所有内容都应为空
• 缓冲区已用部分中的每个项目都应至少与之前的项目一样“大”

现在，我尝试以这种方式实现它：

不幸ccrewrite的是，正在搞乱循环。

用户文档说该方法应该只是对Contract.Invariant. 我真的必须像这样重写代码吗？

这有点难看，尽管它确实有效。（这比我之前的尝试要好得多，请注意。）

我的期望不合理吗？我的不变量不合理吗？

（也在代码合同论坛中作为问题提出。我将自己在这里添加任何相关答案。）

我知道在 DbC 方法中，前置条件和后置条件附加到一个函数。

我想知道这是否也适用于成员函数。

例如，假设我在每个公共函数的开头使用不变量，成员函数将如下所示：

编辑：（清理我的例子）

是否可以仅对全局/泛型函数使用前置条件和后置条件，而只在类中使用不变量？

这似乎有点矫枉过正，但也许我的例子很糟糕。

编辑：

后置条件不只是检查不变量的子集吗？

在上面，我遵循http://www.digitalmars.com/ctg/contract.html的说明，其中指出：“当类构造函数完成时，在类析构函数的开始，在公共之前检查不变量成员运行，并且在公共函数完成后。”

谢谢。

我正在学习一门强调不变量使用的中级编程课程。我以前从未使用过它们，它们似乎需要更多的时间来创建。软件工程行业是否强调使用不变量？

当使用形式方面来创建一些代码时，是否有确定循环不变量的通用方法，或者它会根据问题完全不同？

我目前正在研究“加速 C++”，并在第 3 章中遇到了这个问题：

作者通过解释不变量需要特别注意这一点，因为当输入被读入时x，我们将读取count + 1等级，因此不变量将是不真实的。同样，当我们增加计数器时，sum将不再是上次计数成绩的总和（如果您没有猜到，它是计算学生分数的传统程序）。

我不明白为什么这很重要。当然，对于任何其他循环，类似的陈述都是真的吗？例如，这里是本书的第一个while循环（输出稍后填写）：

一旦我们编写了适当的输出行，在我们增加 之前，不变量肯定是假的r，就像在另一个例子中一样？

是什么让这两个条件不同？

编辑：感谢您的所有回复。我想我已经知道了，但是为了确定，在我选择“已接受的答案”之前，我将让它持续一段时间。到目前为止，所有的回复基本上都同意，所以这似乎不太公平，但我想值得一试。

原始段落，要求如下：

“理解这个循环的不变量需要特别小心，因为 while 中的条件有副作用。这些副作用会影响不变量的真实性：成功执行 cin >> x 使得不变量的第一部分 - 表示我们已经读过count Grades-false。因此，我们必须改变我们的分析来考虑条件本身可能对不变量产生的影响。

我们知道在评估条件之前不变量为真，因此我们知道我们已经阅读了计数等级。如果 cin >> x 成功，那么我们现在已经读取了 count + 1 个等级。我们可以通过增加计数使这部分不变量再次为真。但是，这样做会篡改不变量的第二部分——即 sum 是第一个 count 等级的总和的部分——因为在我们增加 count 之后，sum 现在是第一个 count 的总和 - 1 个等级，而不是第一个计算成绩。幸运的是，我们可以通过执行 sum += x; 使不变量的第二部分为真。这样整个不变量将在随后的旅程中为真。

如果条件为假，则意味着我们的输入尝试失败，因此我们没有获得更多数据，因此不变量仍然为真。因此，我们不必在 while 结束后考虑这种情况的副作用。”

我的意思是，是否有任何寻找类不变量的启发式方法

• 注意……；
• 永远不要依赖……；

也许有共同的建议。

欢迎任何研究现实生活示例的纸上链接。