|
The Omnibus project aims to support the development of reliable software. It is built around the new Omnibus language that is simple to reason about yet familiar to Java programmers. The language is supported by an integrated development environment providing a type checker, automated and interactive static verifiers, a documentation generator and a Java code generator incorporating run-time assertion checks. The tool supports a range of verification techniques from run-time checking and extended static checking of lightweight assertion annotations to full formal verification relative to heavyweight specifications.
Omnibus is a new Object-Oriented language that was specifically designed to be amenable to formal analysis. It was developed as a response to experiences in attempting to formally analyze existing commercial languages like Java. When using those languages, complexities like aliasing greatly complicate verification. Other verification languages are available but often require programming of a different style.
Omnibus is superficially similar to Java, using similar concepts of packages, classes, methods, expressions, statements etc. It is hoped that this will make it easier for developers from a Java-programming background to learn it. The main differences between Omnibus and Java are that Omnibus incorporates a behavioural interface specification language and uses value semantics for objects.
For more information on the Omnibus language, please refer to "The Omnibus Language Reference Manual" and "Writing Specifications in Omnibus, by Example".
 The Omnibus IDE tool provides a range of facilities to assist in the full development process. It incorporates standard facilities for managing files and projects and uses a jEdit component to support syntax highlighting and bracket matching while editing source code. To help detect errors it provides a type checker, automated and interactive verifiers and a code generater which automatically generates run-time assertion checks. Finally, it supports the distribution of the produced applications or components through a bytecode generating compiler, jar builder and interface documentation generator. Applications can be executed through the IDE while jar file packaged components can be integrated into standard Java applications.
|
