论文部分内容阅读
谓词抽象是解决软件模型检查中状态空间爆炸的最有效方法之一,针对Java语言面向对象的特性,描述了一种对Java程序语言中间形式的谓词抽象算法,该算法将Java程序抽象成为布尔程序,抽象过程中处理的Java数据结构包括：赋值语句、条件语句、类对象引用、成员方法和方法调用等。用一个Java程序实例说明了该算法的抽象过程和结果。