| 支持契约式设计的Java静态验证器的研究 |
| |
| 引用本文： | 章程,赵建军,沈备军,陈昊鹏.支持契约式设计的Java静态验证器的研究[J].计算机应用与软件,2008,25(5):134-136. |
| |
| 作者姓名： | 章程 赵建军 沈备军 陈昊鹏 |
| |
| 作者单位： | 上海交通大学软件学院软件工程中心,上海,200030 |
| |
| 摘 要： | 基于对Java编译器的扩展和静态验证技术提出了VeriJava项目,与相关工作相比,它的优点在于从语言层面扩展了Java,并且全面支持动态和静态的契约检查.首先介绍了VeriJava项目的整体架构,及其对Java进行的语言层面的扩展,进而重点讨论了方案的核心部分基于定理证明器的静态验证器的理论和设计,并给出了相关示例.
|
| 关 键 词： | 契约式设计(DBC) Java 静态验证 |
| 修稿时间： | 2006年6月30日 |
RESEARCH OF JAVA STATIC VERIFIER FOR SUPPORTING DESIGN BY CONTRACT |
| |
| Zhang Cheng,Zhao Jian-jun,Shen Bei-jun,Chen Hao-peng.RESEARCH OF JAVA STATIC VERIFIER FOR SUPPORTING DESIGN BY CONTRACT[J].Computer Applications and Software,2008,25(5):134-136. |
| |
| Authors: | Zhang Cheng Zhao Jian-jun Shen Bei-jun Chen Hao-peng |
| |
| Affiliation: | Zhang Cheng Zhao Jianjun Shen Beijun Chen Haopeng(Center for Software Engineering,School of Software,Shanghai Jiaotong University,Shanghai 200030,China) |
| |
| Abstract: | 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... |
| |
| Keywords: | Design by Contract(DBC) Java Static verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
