ESC/Java

ESC/Java （以及最近的ESC/Java2 ），“ Java的扩展静态检查器”，是一种编程工具，试图在编译时在Java程序中查找常见的运行时错误。 ESC/Java中使用的基本方法称为扩展静态检查，这是一个集体名称，指的是静态检查各种程序约束的正确性的一系列技术。例如，整数变量比零更大，或者位于数组的边界之间。该技术是在ESC/Java（及其前身ESC/Modula-3）中开创的，可以将其视为一种扩展的类型检查形式。扩展的静态检查通常涉及使用自动定理供体，并且在ESC/Java中，使用了简化的定理供体。

ESC/Java既不声音也不完整。这是故意的，旨在减少向程序员报告的错误和/或警告的数量，以便使工具在实践中更有用。但是，这确实意味着：首先，ESC/Java的程序将错误地认为是不正确的（称为假阳性）；其次，它将认为是正确的程序（称为假阴性）。后一类中的示例包括模块化算术和/或多线程引起的错误。

ESC/Java最初是在Compaq系统研究中心（SRC）开发的。 SRC于1997年启动了该项目，此前其原始的扩展静态检查器ESC/Modula-3于1996年结束。2002年，SRC发布了ESC/Java和相关工具的源代码。 ESC/Java的最新版本基于Java建模语言（JML）。用户可以通过特殊格式的评论或布拉格马斯来注释程序来控制检查的数量和种类。

Nijmegen大学系统组的安全性发布了ESC/JAVA2的Alpha版本，ESC/JAVA2是ESC/Java的扩展版本，该版本在2004年之前处理JML规范语言。从2004年到2009年，ESC/JAVA2开发由KindSoft Wardewware研究小组管理在都柏林大学学院，该学院于2009年移居哥本哈根大学，并于2012年搬到丹麦技术大学。多年来，ESC/Java2获得了许多新功能，包括具有多个定理抛弃和与Eclipse集成的推理能力。

ESC/Java2的继任者OpenJML可用于Java 1.8。该来源可从https://github.com/openjml获得

也可以看看