algorithm - 程序员如何在 TopCoder 或其他竞赛中测试他们的算法？

Question

在TopCoder或ACM ICPC的比赛中编写中高难度程序的优秀程序员，在提交前必须确保算法的正确性。

虽然他们提供了一些示例测试用例来确保正确的输出，但是它如何保证程序会正确运行？他们可以自己写一些测试用例，但不可能在所有情况下都通过人工计算知道正确答案。他们是怎么做到的？

更新:看起来，在竞争环境的严格约束下，不太可能分析和保证算法的结果。但是，如果有任何手册，在解决此类问题时采用了更常见的特征 - 应该足以回答这个问题。诸如最佳实践之类的东西..

Answer 1

在比赛中，顶尖的程序员有足够的经验来阅读问题，并想出一些应该捕获输入的大部分可能性的测试用例。
它通常会捕获大部分错误 - 但它并非 100% 安全。

但是，在现实生活中的关键应用程序(例如飞机或核 react 堆上的关键系统)中，有一些方法可以证明某些代码片段执行了它应该执行的操作。

这是formal verification的领域- 这在比赛期间完成起来太复杂和耗时，但对于某些系统来说，它被使用是因为不能容忍错误。

---

一些附加信息:
形式化验证主要由两部分组成:

1. 手动验证 - 在这里我们使用证明系统，例如 Hoare logic并手动证明该程序执行我们希望它执行的操作。
2. 自动 model checking - 将问题建模为状态机，并使用模型检查工具来验证模块是否做了它应该做的事情(或者没有做“坏事”)。
   指定“它应该做什么”通常用temporal logic来完成。 .
   这也常用于验证硬件模型的正确性。例如英特尔使用它来确保他们不会得到 floating point bug再次。