为了避免软件模型检查中状态空间爆炸的问题，谓词抽象成为了Java程序中较为有效的解决方法之一。本文详细描述了针对Java语言面向对象的特性，一种对Java程序语言中间形式的谓词抽象算法。该算法将Java程序抽象成为布尔程序，并涉及到的Java数据结构包括：赋值语句、条件语句等。