计算机应用与软件
計算機應用與軟件
계산궤응용여연건
COMPUTER APPLICATIONS AND SOFTWARE
2008年
5期
134-136
,共3页
章程%赵建军%沈备军%陈昊鹏
章程%趙建軍%瀋備軍%陳昊鵬
장정%조건군%침비군%진호붕
契约式设计(DBC)%Java%静态验证
契約式設計(DBC)%Java%靜態驗證
계약식설계(DBC)%Java%정태험증
基于对Java编译器的扩展和静态验证技术提出了VeriJava项目,与相关工作相比,它的优点在于从语言层面扩展了Java,并且全面支持动态和静态的契约检查.首先介绍了VeriJava项目的整体架构,及其对Java进行的语言层面的扩展,进而重点讨论了方案的核心部分基于定理证明器的静态验证器的理论和设计,并给出了相关示例.
基于對Java編譯器的擴展和靜態驗證技術提齣瞭VeriJava項目,與相關工作相比,它的優點在于從語言層麵擴展瞭Java,併且全麵支持動態和靜態的契約檢查.首先介紹瞭VeriJava項目的整體架構,及其對Java進行的語言層麵的擴展,進而重點討論瞭方案的覈心部分基于定理證明器的靜態驗證器的理論和設計,併給齣瞭相關示例.
기우대Java편역기적확전화정태험증기술제출료VeriJava항목,여상관공작상비,타적우점재우종어언층면확전료Java,병차전면지지동태화정태적계약검사.수선개소료VeriJava항목적정체가구,급기대Java진행적어언층면적확전,진이중점토론료방안적핵심부분기우정리증명기적정태험증기적이론화설계,병급출료상관시례.
