问题标签 [proof-of-correctness]

我了解到 Bellman-Ford 算法的运行时间为 O(|E|*|V|)，其中 E 是边数，V 是顶点数。假设该图没有任何负加权循环。

我的第一个问题是，我们如何证明在 (|V|-1) 次迭代中（每次迭代检查 E 中的每条边），在给定特定起始节点的情况下，它会更新到每个可能节点的最短路径？有没有可能我们已经迭代了 (|V|-1) 次，但仍然没有得到到每个节点的最短路径？

假设算法的正确性，我们实际上可以做得更好吗？在我看来，并非所有边在特定图中都具有负权重。Bellman-Ford 算法似乎很昂贵，因为每次迭代都要经过每个边缘。

我无法理解如何找到循环不变量并为它们编写正式的语句。因此，循环不变量只是在循环的每次迭代之前和之后立即为真的条件。看起来代码正在执行交换：如果数组中的以下元素大于当前元素，则切换位置。我的意思是从循环不变量的定义来看，它听起来真的是 i < 100 因为循环运行必须是这样，但我不太明白。非常感谢一些澄清。

我发现The Hitchhiker's Guide to the Programming Contests中提到的算法（注意：此实现假定列表中没有重复项）：

这是一种在 O(NlogN) 中找到最长递增子序列的算法。如果我尝试使用很少的测试用例来处理它，它似乎可以工作。但我仍然无法弄清楚它的正确逻辑。此外，它对我来说看起来并不那么直观。

谁能帮我深入了解为什么这个算法可以正常工作？

正如标题所示，我的问题涉及证明 Coq 中算术表达式的惰性求值的正确性和完整性。我想证明的定理共有三个：

1. 计算只给出规范表达式作为结果

   Theorem Only_canonical_results: (forall xy: Aexp, Comp xy -> Canonical y)。

2. 正确性：计算关系保留表达式的表示

   Theorem correct_wrt_semantics: (forall xy: Aexp, Comp xy -> IN (denotation x) (denotation y))。

3. 每个输入都会导致一些结果。

   Theorem Comp_is_total: (forall x:Aexp, (Sigma Aexp (fun y => prod (Comp xy) (Canonical y))))。

必要的定义可以在下面附加的代码中找到。我应该明确表示我是 Coq 的新手；更有经验的用户可能会立即注意到。可以肯定的是，我所写的大部分或什至所有背景材料都可以在标准库中找到。但是，话又说回来，如果我确切地知道从标准库中导入什么来证明所需的结果，我很可能不会在这里打扰你。这就是为什么我将我目前拥有的材料提交给你，希望有热心的人可以帮助我。谢谢！

我们可以通过这种方式将下面文档中两个字符串的 LCS 算法扩展为三个字符串吗？

http://www.columbia.edu/~cs2035/courses/csor4231.F13/lcs.pdf - 文件，第 5 页第 2 点。

1. 如果 xm != yn 或 xm != tj 则 zk != xm 意味着 Z 是 Xm-1 和 Y 和 T 的 LCS。

“如果 zk != xm，那么 Z 是 Xm-1 和 Y 和 T 的公共子序列。如果存在长度大于 k 的 Xm-1 和 Y 和 T 的公共子序列 W，那么 W 也是一个公共子序列X m 和 Y 和 T 的子序列，与 Z 是 X 和 Y 和 T 的 LCS 的假设相矛盾。"

其中 T = 是我们的第三个字符串

我试图解决以下问题，但我无法检查它....或者 wolfram 会这样做吗？我不知道我对运算符（范围）的处理是否是 occrect...你知道吗？对于所有 x：颠倒的 A 运算符（通用性）

证明：

我试图更全面地了解动态编程中最优子结构属性的使用，但我对为什么我们必须证明问题的任何最优解决方案都包含子问题的最优解决方案视而不见.

证明某个问题的某个最优解具有这个性质，然后用​​它来论证由于我们的递归算法构建的解至少与最优解一样好，它本身就是最优的，这难道还不够吗？换句话说，我没有发现在我们的算法的正确性论证中，我们需要所有最优解都包含子问题的最优解。

澄清：

CLRS 对最优子结构的定义说：“如果问题的任何最优解包含子问题的最优解，则问题表现出最优子结构”。

为什么说“如果某个问题的某个最优解包含子问题的最优解，则该问题表现出最优子结构”是不够的？

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

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？以下算法找到最大值是否正确？

答案必须基于算法最弱前提的计算。

你如何验证这一点？似乎很简单。

谢谢。

我有一个非常简单的函数，它应该以给定的时间单位计算两个日期之间的时间量，例如：getPartialPeriod(January 1, February 15, months)将导致1.5.

我真的很纠结如何证明它——我从循环开始，因为我认为这是最困难的部分。我定义了许多 Hoare 三元组和循环不变量，却发现它们都没有用。我会很感激我能得到的所有帮助。

函数伪代码：

PS请忽略这似乎是一个愚蠢的实现 - 这并不重要。

不要误会我关于在在线法官上发布问题的问题。我只想知道如何证明解决方案的正确性。以下是Wine 交易问题。它说在单位距离内有一排房子，每个房子都想卖或买酒。总需求=总供给。交易中完成的工作是涉及的酒量乘以距离。问题是在最低限度的工作中满足所有房屋的需求。建议的解决方案是第一个卖家（比如说从行的右侧开始）卖给第一个买家（金额= min（卖家，买家））（这是贪婪的选择），然后解决剩下的问题。如何正式证明这是正确的？