Enhancing the Expressiveness of the CleanJava Language

The CleanJava language is a formal annotation language for Java to support Cleanroom-style functional program verification that views a program as a mathematical function from one program state to another. The CleanJava notation is based on the Java expression syntax with a few extensions, and thus its vocabulary is somewhat limited to that of Java. This often makes it difficult to specify the rich semantics of a Java program in a succinct and natural way that is easy to manipulate for formal correctness reasoning. In this paper we propose to make the CleanJava language more expressive by supporting user-defined mathematical functions that are introduced solely for the purpose of writing annotations. A user-defined function is written in a notation similar to those of modern functional programming languages like SML and Haskell and has properties such as polymorphism and type inference. We also explain how the notion of functions fits in the object-oriented world of Java with concepts like inheritance and method overriding. User-defined functions not only enrich the vocabulary of CleanJava but also allow one to tune the abstraction level of annotations. One contribution of our work is bringing the notion of functions as found in modern functional programming languages to an object-oriented programming language in the context of writing annotations, thus blending the benefits of two programming paradigms