问题标签 [correctness]

我一直在重构一些相当笨拙的代码，并遇到了以下相当奇怪的结构：

...我想知道这是否有任何可能的意义。

我将其更改为：

我确实启动了一个解释器并实际尝试了第一个构造......它似乎只在值全部为假并且这些假值中的最后一个为无时才有效。（换句话说，CPython 的实现似乎从or表达式链中返回第一个真值或最后一个假值）。

我仍然怀疑正确的代码应该使用在 2.5 中添加的any()或all()内置插件（有问题的代码已经需要 2.7）。我还不确定哪个是首选/预期的语义，因为我刚刚开始这个项目。

那么在任何情况下这个原始代码是有意义的吗？

问题是：

我想出的算法是这样的：

到目前为止是否正确？但我不确定如何证明它的正确性......我的尝试看起来只是用英文重写代码......

对于第一个如果：我们总是可以使用 1 个面额 i 的硬币来解决 amt=i。对于第一个 else if：如果我们有一个不使用当前面额的 amt 解决方案，我们可以重用该解决方案。对于第二个 else if：如果可以使用当前面额（<= amt），并且不使用面额，我们可以...

对于复杂性：表的大小为 nA。每个单元格需要 O(1) 时间来填充。有人可以帮我指出正确的方向吗？

我试图找到一个循环不变量，以便我们可以证明这个程序部分正确：

我真的被困住了。到目前为止，我尝试过的一些不变量是：

和

我真的很感激一些建议。

我正在推理 Hoare Logic 的练习。

我应该找到满足三元组的所有布尔表达式B和所有程序S，假设 的评估不能修改存储，但执行可以修改它并改变 的值。P{true} if B then S; if B then P; {a >= 0}BSB

特别是，我不知道我能说什么a，因为它只存在于后置条件中，我从未找到过这样的例子。

谢谢你的帮助！

给你两个数组，第一个数组包含表示人的高度的整数，第二个数组包含在他面前站着多少个身高比他大的人并形成一个队列。

• 高度是唯一的，这意味着没有两个人可以拥有相同的高度。

例子-

答：3 2 1

乙：0 1 1

这意味着在身高3的人面前没有人站立，身高2的人面前有一个比他高的人，类似于身高1的人。你安排他们的任务应该是。3 1 2

我的方法

1.根据频率（高人的数量）对人员进行排序。

2.现在将每个人的位置固定在适当的位置。例如：

3 1 2 4

0 2 1 0

排序后

3 4 2 1

0 0 1 2

现在我们看到第一人和第二人在正确的位置，所以我们将第三人移动到正确的位置，即第二人（基础索引 1），因为他面前只有一个更高的人。

3 2 4 1

0 1 0 2

现在对于第 4 个人，我们只需将其放在第 3 位

3 2 1 4

0 1 2 0

最终答案。

我认为它具有 O(n^2) 复杂度。我们可以做得更好，该算法的正确性如何？

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

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

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

G 是一个只有正权重的连通无向图。S是最短路径树（不一定是G的SPT）。所以我要设计一个算法来检查图S是否是图G的最短路径树。

我的算法是这样的......

在 G 和 S 上运行 Dijkstra 算法（返回图形，而不是最短路径）。检查每个顶点的 dist(v) 值，如果都相同，则 S 是 G 的最短路径树。

我不知道这个算法是否有效，但我认为它是合理的。如果是真的，我如何证明它的正确性，如果不是，反例会很有帮助吗？

* 我也在 CS Exchange 上发布了这个 *

我开始严重依赖haskell 的类型系统来避免错误，并且正在寻找它是否也可以用来确保（弱？）形式的代码正确性。

我想到的代码正确性形式如下：

如果保证为 type的任何输入产生 type的输出，则该函数f :: a -> b是正确的。对于众所周知的函数 head ( )，这显然失败了。fbahead:: [a] -> a

我知道类型系统无法保证这种形式的正确性的一种方法是代码使用错误（error :: Char -> a）。错误函数几乎覆盖了整个类型系统，所以我想避免使用这个函数，除非明确表示。

我的问题有两个：

1. 除了错误之外，还有哪些其他函数（或 haskell 片段）是 Haskell 类型系统的例外？

2. 更重要的是，有没有一种方法可以禁止在 Haskell 模块中使用此类功能？

非常感谢！

我最近和我的教授讨论了如何处理基本的 jdbc 连接方案。假设我们要执行两个查询，这是他提出的

我不喜欢这种方法，对此我有两个问题：

1.A）我认为，如果在我们做“其他事情”的地方抛出任何异常，或者在该行中，或者在rs.close()方法结束s2.close()时s1不会被关闭。我说得对吗？

1.B）教授一直要求我明确关闭结果集（即使声明文档明确表示它将关闭结果集）她说 Sun 推荐它。有什么理由这样做吗？

现在这是我认为是同一件事的正确代码：

2.A）这段代码正确吗？（是否保证方法结束时全部关闭？）

2.B）这是非常大且冗长的（如果有更多的语句，它会变得更糟）是否有任何更短或更优雅的方法可以在不使用 try-with-resources 的情况下做到这一点？

最后这是我最喜欢的代码

3）这段代码正确吗？我认为我的教授不喜欢这种方式，因为没有明确关闭 ResultSet，但她告诉我，只要在文档中清楚地表明所有内容都已关闭，她就可以接受。您能否提供任何带有类似示例的官方文档链接，或者根据文档显示此代码没有问题？

今天我写了一个算法来计算一个给定的代表离散函数的点数组的快速傅里叶变换。现在我正在尝试测试它是否有效。我已经尝试了大约十几种不同的输入集，它们似乎与我在网上找到的示例相匹配。但是，对于我的最终测试，我给它输入 cos(i / 2)，i 从 0 到 31，根据我使用的求解器，我得到了 3 个不同的结果。我的解决方案似乎是最不准确的：

这是否表明我的算法存在问题，或者仅仅是数据集相对较小的结果？

我的代码如下，以防万一：