支持契约式设计的Java静态验证器的研究  

RESEARCH OF JAVA STATIC VERIFIER FOR SUPPORTING DESIGN BY CONTRACT

作　　者：章程[1] 赵建军[1] 沈备军[1] 陈昊鹏[1] 

机构地区：[1]上海交通大学软件学院软件工程中心,上海200030

出　　处：《计算机应用与软件》2008年第5期134-136,共3页Computer Applications and Software

摘　　要：基于对Java编译器的扩展和静态验证技术提出了VeriJava项目,与相关工作相比,它的优点在于从语言层面扩展了Ja-va,并且全面支持动态和静态的契约检查。首先介绍了VeriJava项目的整体架构,及其对Java进行的语言层面的扩展,进而重点讨论了方案的核心部分基于定理证明器的静态验证器的理论和设计,并给出了相关示例。We raise the VeriJava project based on extension of Java complier and static verification techniques. Compared with related works, its advantages are language level extension of Java and comprehensive supporting for both dynamic and static contract checking. In this paper, we first give an introduction to the architecture of VeriJava project and its language extension of Java, then we discuss in detail on theory and design of theorem prover based static verifier, which is the core part of our project, with related examples.

关 键 词：契约式设计(DBC) JAVA 静态验证 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论] TG519.1[自动化与计算机技术—计算机科学与技术]