SpecJ : Towards Adding Contracts to Java

概要

論文の詳細を見る
SpecJ is a programming system for supporting Design by Contract (DBC) in Java. SpecJ consists of an object-oriented programming language called SpecJ, a compiler for compiling programs written in SpecJ to Java bytecodes and also a static verifier for assuring that the code is consistent with its specifications. SpecJ is a simple and practical extension to Java, with just a few new language constructs, to support pre- and postconditions for methods and class invariants. SpecJ also supports class specification inheritance. This paper discusses the goal and the overall programming approach of SpecJ. The paper also gives examples of SpecJ programs. On one hand, SpecJ provides a way to Java with assertions (pre- and postconditions, and class invariants), supporting runtime checking such as debugging and testing of SpecJ programs. On the other hand, SpecJ offer the possibility of automatic compile-time analysis (verification) for SpecJ programs such as checking the code of a method against its specification, checking that the specification of a subclass is compatible with the specification of its superclass.
一般社団法人情報処理学会の論文
2005-07-28