【VC++开源代码栏目提醒】:以下是网学会员为您推荐的VC++开源代码-ESC/JAVA & Theorem Proving - 计算机教材,希望本篇文章对您学习有所帮助。
ESC/JAVA Theorem Provingwuqian08sei.pku.edu.cn12ESC/JAVA345ESC/JAVA26??ESC/JAVA Extended Static Checker for JAVAJAVApragma??verification-condition generation automatic theorem proving-1??用户向程序中添加可选的pragma,ESC/JAVA将检查程序和这些pragma的一致性。
??用pragma记录
设计约束,如变量不能为空、前置条件、后置条件。
??支持模块化检查。
当检查一个方法体m时,工具不检查m所调用的方法r的方法体,仅检查m的调用是否符合r的规范:pragma如requires、ensures;方法签名;return;throws。
??当缺少源文件时,用户可以将pragma写到.spec文件中。
当类T用到了类U,工具需要获取类U的不变式以及U中方法的规范。
如果只有U.class文件,那么工具将仅读取方法的签名等信息作为U的约束。
用户可以通过向U.spec文件中添加pragma提供额外的不变式和规范。
-2??ESC/JAVA只能检查JAVA1.2;ESC/JAVA2只能检查JAVA1.4。
??工具对潜在的运行时错误报出警告Warning。
??工具目前只检查方法体,忽略静态初始化器、匿名类等。
??工具把JVM抛出的运行时异常作为运行时错误。
如NullPointerException ClassCastException等。
??工具对不符合语法的程序报错Error:编译错误或者pragma的书写不符合规范。
-3??ESC/JAVA不是完美的。
??产生漏报unsoundness工具不检查算术溢出和无限循环等缺陷,也不检查功能的正确性;工具检查的缺陷也可能产生漏报。
??产生误报incompleteness工具报出警告,仅仅意味着工具无法证明
程序不会出错。
??用户添加pragma,可以改善漏报和误报的产生。
12ESC/JAVA345ESC/JAVA261-2-ESC/JAVA??escjava Bag.java2-ESC/JAVA2Null3IndexTooBig1Null4Null5IndexNegative3-requires??对于第一个警告input可能为null的处理方法:1修改构造函数,加入判空操作2添加requires??requires指定方法调用的前置条件:在方法调用之前,requires后面的布尔表达式必须为真。
??当检查一个包含前置条件的方法体时,工具假定方法体内部前置条件都为真;当检查对包含前置条件的方法的调用时,对于调用者不满足被调用者的前置条件的情况,工具报错。
4-non_null??对于第二个警告ai1??更多信息参见:ESC/JAVA-??操作:对每个方法R,调用自动定理证明器Simplify证明:其中,
VC是R的验证条件,BP是特定于类型的基础断言,UBP是通用的基础断言universal background predicate,它描述了Java语义中的一般事实,如任何类都是Object的子类等。
??上式当且仅当R没有错误时为真。
??对于逻辑L的算子calculusC包含一个公理集合A和一个推导规则集合R。
公理是L中的公式,表述一些逻辑运算的基本性质。
推导规则的一般形式:??对L中的公式的基于前提的集合的一个推导是一个有限的公式序列,对于所有的,或者,或者将推导规则集合R作用到可以得到。
这样就称公式是前提的一个定理。
??自动定理证明器通过
搜索公式序列完成对L的证明,分为正向推导和反向规约。
ESC/JAVA-??操作:处理定理证明器的结果,当证明器无法证明验证条件为真时,报出警告。
??通过反例的上下文进行错误的定位。
??通过在处理的每个阶段携带源
代码的位置信息,ESC/JAVA能够为每个警告关联其在源码中的位置。
12ESC/JAVA345ESC/JAVA261??ESC/JAVA报出的警告共有21种:??1 ArrayStore-ArrayStoreException ??2 Assert ??3Cast-ClassCastException ??4Deadlock??5Exception??6 IndexNegative-IndexOutOfBoundsException??7 IndexTooBig-IndexOutOfBoundsException??8 Invariant ??9 LoopInv??10 NegSize-NegativeArraySizeException??11 NonNull2??12 NonNullInit??13 Null-NullPointerException ??14 OwnerNull ??15 Post ??16 Pre ??17 Race ??18 Reachable ??19 Unreadable ??20 Uninit ??21 ZeroDiv-ArithmeticException -1??竞争条件:多个线程同时访问一个变量,且存在线程试图修改这个变量。
??monitered_by L:被修饰的域是被L中的锁监视的共享变量。
lockset代表当前线程拥有的所有被作为锁的对象;locksetx为真表示对象x在lockset中。
??避免竞争条件:1不允许线程T读取变量,除非T拥有至少一个L中的非空锁。
2不允许线程T修改变量,除非L中至少有一个锁非空,且T拥有L中的所有非空锁。
-2??变量声明:??
代码片段:-1??避免死锁:用户指定锁的偏序关系,工具检查锁的获取是否按照递增的顺序。
-2??用户指定锁的偏序关系:??如果用户不添加相关注释,工具则无法证明死锁不存在;因此,缺省情况下工具不检查死锁。
12ESC/JAVA345ESC/JAVA26??使用ESC/JAVA检查Javafe,它共有41KLOC,2331个方法,使用667MHz的Alpha处理器:??ESC/JAVA是基于注释的检测工具。
??对
Javafe的注释结果表明:??每一千行
代码大约需要40-100个注释。
??一个程序员在一个小时内可以对一个现有的程序的300-600行
代码添加注释。
??推荐做法:在开发阶段中,尽早书写注释并运行ESC/JAVA进行缺陷的检查。
12ESC/JAVA345ESC/JAVA26??ESC/JAVA最初是由Compaq公司现在的HP的System ReseachCenter研发的,最终的ESC/JAVA发布于2002年,支持Java1.2。
??随后,Compaq公司停止了对此工具的维护和更新。
另外三个人开始在ESC/JAVA的基础上研发ESC/JAVA2。
??2005年9月,ESC/JAVA2被并入项目Mobius MobilityUbiquity Security,2005年10月1日,得到HP公司的许可,ESC/JAVA2完全
开源。
??目前Mobius的一部分被称为ESC/JAVA3。
ESC/JAVA2??ESC/JAVA2对ESC/JAVA的改进主要在以下三个方面:??更新ESC/JAVA的解析器,使其可以和当前的JML和JAVA一致。
最新版本的ESC/JAVA2今年11月发布的稳定版,支持JAVA1.4,部分支持JAVA1.5。
??对工具包装,方便用户的使用和获取源
代码。
??扩展工具支持的JML 标记。
12ESC/JAVA345ESC/JAVA26wuqian08sei.pku.edu.cn