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

• 作者: 沈备军 章程 赵建军 陈昊鹏
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 契约式设计(DBC) Java 静态验证
• 年，卷（期）: 2008,（5）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 134-136
• 页数: 3页
• 分类号: TP3
• 字数: 3321字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386X.2008.05.053

摘要

基于对Java编译器的扩展和静态验证技术提出了VeriJava项目,与相关工作相比,它的优点在于从语言层面扩展了Java,并且全面支持动态和静态的契约检查.首先介绍了VeriJava项目的整体架构,及其对Java进行的语言层面的扩展,进而重点讨论了方案的核心部分基于定理证明器的静态验证器的理论和设计,并给出了相关示例.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈昊鹏	上海交通大学软件学院软件工程中心	25	124	7.0	9.0
2	赵建军	上海交通大学软件学院软件工程中心	12	35	3.0	5.0
3	沈备军	上海交通大学软件学院软件工程中心	36	269	9.0	15.0
4	章程	上海交通大学软件学院软件工程中心	6	80	3.0	6.0