最近我读了很多关于形式验证的文章，我对这个话题很着迷。但是我无法弄清楚以下内容：
形式验证需要形式规范，那么当程序没有形式规范时，如何在编译器中的任何源代码上使用抽象解释？
从看起来正确的外语文本翻译（而且似乎不需要正式的规范。）
如果一个程序由它的控制流程图表示，那么每个分支都表示一个程序状态（可以不止一个 - 例如，在循环中，一个分支被遍历多次）并且抽象解释创建了近似于该状态集的静态语义。
这里有一篇关于抽象解释作为形式验证技术的文章：http ://www.di.ens.fr/~cousot/publications.www/Cousot-NFM2012.pdf
可以通过为一种语言构建解释器来进行“具体解释”，该解释器根据语言规范手册计算结果。（语言手册是非正式的这一事实使这种解释器的正确性永远受到质疑）。
抽象解释只需要对程序语义有很好的理解，并且知道什么是值得抽象的。您可以通过使用上面的解释器，并将实际计算替换为计算的抽象来实现这一点，例如，您可以决定将所有整数值表示为“正”、“零”、“负”或“未知”。您仍然可以使用它进行计算，现在可以产生定性结果。更重要的是，您可以使用它进行计算，而无需实际的程序输入（可能只是抽象值）。我注意到抽象解释器在正式意义上也是完全不可信的，因为您仍在使用非正式参考手册作为语言将要做什么的指南进行计算。
现在，通过运行这样一个抽象程序，您可能会发现它会出错（例如，取消引用空值），因为控制该空值的变量不是“未定义”。在这种情况下，您可以建议程序中存在错误；您可能不对，但这可能会产生有用的结果。
实践中的抽象解释无法告诉您程序正式计算的内容，因为您仍在使用非正式的参考手册。如果手册要成为正式文档，并且您的抽象解释器是通过可证明的正确步骤派生的，那么我们可能会同意，程序的抽象解释是一种规范，它以程序实际执行的抽象为模。
抽象解释没有提供对程序意图的正式规范的访问。因此，您不能单独使用它来证明程序在规范方面“正确”。
抽象解释是一种用于静态地了解软件行为方式的方法。它永远不会单独出现——总是有一些目标，其中包括抽象解释作为其组成部分之一。
这种目标的一个例子是形式验证，其中使用静态技术（例如抽象解释）来获取有关代码的信息，然后将其与提供的规范进行比较。这就是验证需要规范的原因——你需要一些东西来比较它。