问程序分析精度

EN

一般来说，确定程序中的哪一条路径，以及哪一条--不--的任务是无法确定的。很有可能，像在您的示例中一样，一个特定的表达式可以被证明具有特定的值。然而，“一般”和“不可判定”这两个词表明，您不能编写一种算法，可以每次计算值。

此时，分析算法可以是乐观的，也可以是悲观的。乐观的人可以选择8并且很好--它认为在运行时x可能会得到这个值。它还可以选择7 --“谁知道，也许，x会是7”。但是，如果分析必须是健全的，并且它不能确定条件的值，那么它应该假设第一个分支可以在一个执行过程中得到，而第二个分支可以在另一个执行期间进行，所以x可以是7或8。

换句话说，在稳健性和精确性之间有一种权衡。或者，实际上，在稳健性、精确性和可判定性之间。后一个属性告诉分析是否总是终止。现在，你必须选择所需要的：

• 决策--这是编译器和代码分析器的常见选择，因为您希望在有限的时间内得到关于程序的答案。但是，验证助理可以启动一些进程，这些进程可以运行到指定的时间限制，如果限制没有设置，则永远由用户来停止它并尝试else.
• Soundness --这是编译器的常见选择，因为您希望得到与语言规范相匹配的答案。代码分析器更灵活。其中许多是不健全的，但正因为如此，他们可以在有限的时间内发现更多的潜在问题，让开发人员来解释。我相信你提到的例子谈到了声音analysis.
• Precision -这是一个罕见的财产。编译器和代码分析器应该是悲观的，因为否则一些不正确的代码可能会潜入其中。但这可能是可以参数化的。例如，如果编译器/分析器支持常量传播和折叠，并且示例中的所有变量都设置为条件之前的一些已知常量，那么它可以计算出它之后的x的确切值，并且是完全精确的。