7

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

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

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

4

3 回答 3

8

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

然而，在现实生活中的关键应用程序（例如飞机或核反应堆上的关键系统）中，有一些方法可以证明某些代码完成了它应该做的事情。

这是形式验证的领域- 这太复杂且太耗时，无法在比赛中完成，但对于某些系统来说，因为不能容忍错误而使用它。

一些附加信息：
形式验证基本上由两部分组成：

  1. 手动验证 - 在这里我们使用证明系统，例如Hoare 逻辑，并手动证明程序做了我们想要它做的事情。
  2. 自动模型检查- 将问题建模为状态机，并使用模型检查工具来验证模块是否做了它应该做的事情（或者没有做一些“坏事”）。
    指定“它应该做什么”通常是用时序逻辑完成的。
    这通常也用于验证硬件模型的正确性。例如，英特尔使用它来确保他们不会再次遇到浮点错误。
于 2013-07-11T09:18:16.613 回答
3

想象一下，假设您是一名顶级程序员。这意味着您知道一堆算法，并且在实施它们时不会三思而后行。您知道如何修改已知算法以满足问题的需求。您擅长估算时间和复杂性，并且您期望在最坏的情况下您的定制算法将在时间和内存限制内运行。
在这个级别你只需思考并使用草稿本大约五到十分钟，并在开始编码之前有一个超级清晰的算法。一旦你完成编码，你点击编译，通常不会出现编译错误。因为代码非常直观给你。然后根据使用的算法和使用的数据结构，您预计可能存在以下问题之一。

  1. 一个角落案例
  2. 溢出问题

极端情况基本上就像您为一般情况编写的代码，但是当说 N=1 时，答案与其他情况不同。因此，您通常将其写为特殊情况。溢出是指中间值或结果溢出数据类型的限制。

您记下此时出现的任何问题，并在挑战阶段使用此数据（如在 TopCoder 中）。
一旦你检查了这两个，你点击提交。

于 2013-07-11T14:56:49.053 回答
2

Top Coder 有一个时间元素，因此不可能测试该约束内的每个组合。他们可能会尽力而为，其余的则依靠经验，就像在现实生活中所做的那样。我不知道有没有可能保证一段重要的代码永远没有错误。

于 2013-07-11T09:15:45.443 回答