VeriJava

From stap
Jump to: navigation, search
  • Motivation
The principle of Design by Contract (DBC) was originally introduced by Meyer for supporting reliable software development. The current research so far in supporting the principle of DBC in Java is focused mainly on the development of specific specification languages and tools. However, few research has been focused on supporting DBC in Java from a language design viewpoint. Until recently, a few programming languages, e.g., Eiffel and Spec# implement pre- and postconditions, class invariants in executable code so that they are checked at run time. However, Java does not have such support, so programmers who want to use pre- and postconditions, and class invariants in Java often write comments documenting the conditions. This is not an ideal situation because the comments are not verified automatically, and they may not even be consistent with the actual code. This motivates us to design a new programming system that extends Java with contract specifications such as preconditions, postconditions, and class invariants so that programmers who write programs in Java can easily write contracts as well.
VeriJava programming system consists of an object-oriented programming language called VeriJava, a compiler for compiling programs written in VeriJava to Java bytecode, and a static verifier for assuring that the VeriJava code is consistant with its specifications. VeriJava language is a simple and practical extension to Java language, with just a few new language constructs, to express and support assertions such as pre- and postconditions for methods and class invariants within Java language. VeriJava also supports class specification inheritance.
VeriJava is a project that aims at developing a new programming system for adding contracts to Java from a language design viewpoint.
Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox