扩展静态检查

扩展静态检查（ESC）是计算机科学中对各种程序约束的正确性进行静态检查的一系列技术的总称。ESC可以被认为是类型检查的一种扩展形式。与类型检查一样，ESC是在编译时自动进行的（即无需人工干预）。这使它区别于更多的软件形式化验证的一般方法，后者通常依赖于人类产生的证明。此外，它提倡实用性而不是合理性，因为它的目的是以引入一些假阴性（真正的ESC低估错误，但不需要程序员注意，或不被ESC所针对）为代价，xxx减少假阳性的数量（被高估的错误，但不是真正的错误，即ESC超过严格性）。ESC可以识别一系列目前在类型检查器范围之外的错误，包括除以0、数组出界、整数溢出和空解定义。扩展静态检查中使用的技术来自计算机科学的各个领域，包括静态程序分析、符号模拟、模型检查、抽象解释、SAT求解以及自动定理证明和类型检查。扩展静态检查一般只在程序内而不是程序间进行，以便扩展到大型程序。此外，扩展的静态检查旨在通过利用用户提供的规范，以前后条件、循环不变性和类不变性的形式报告错误。扩展的静态检查器通常通过在程序内传播xxx的后置条件（或者最弱的前置条件）来操作，从前置条件（或者后置条件）开始的方法。在这个过程中的每一个点上，都会产生一个中间条件，以捕捉到该程序点上的已知内容。这与该点上的程序语句的必要条件相结合，形成一个验证条件。这方面的一个例子是一个涉及除法的语句，其必要条件是除数为非零。

由此产生的验证条件实际上是：考虑到此时的中间条件，必须得出除数为非零的结论。所有的验证条件都必须被证明是错误的（因此通过排除第三种方法是正确的），以便一个方法能够通过扩展的静态检查（或无法发现更多的错误）。通常情况下，某种形式的自动定理检验器被用来排出验证条件。扩展静态检查是在ESC/Modula-3以及后来的ESC/Java中开创的。它起源于更简单的静态检查技术，如静态调试或Lint（软件）和FindBugs。其他一些语言也采用了ESC，包括Spec#和SPARKada以及VHDLVSPEC。然而，目前还没有一种广泛使用的软件编程语言在其基本开发环境中提供扩展静态检查。