Friday, October 12, 2012: 8:00 PM
6C/6E (WSCC)
The CleanJava language is a formal annotation language for Java to
support functional program verification. In functional verification, a
program is viewed as a mathematical function that maps one program
state to another, and thus proving the correctness of a program is
essentially comparing two mathematical functions, the function
implemented by the program and its specification. Since the CleanJava
notation is based on Java expressions with extensions such as
mathematical structures like sets and sequences, its vocabulary is
limited that of Java. In this paper, we propose to make the CleanJava
language more expressive by enhancing its extension mechanism. Our
approach is to support user-defined mathematical functions, functions
introduced by the user for the purpose of writing annotations. They
not only enrich the vocabulary of CleanJava but also allow one to tune
the abstraction level of CleanJava annotations. The user-defined
mathematical functions are polymorphic---meaning that they may be
applied to values of different types---and the signatures of the
functions need not be declared. Both the signatures of user-defined
functions and the types of CleanJava expressions are inferred
statically. Polymorphic functions allow one to write generic and
reusable functions, and resulting annotations become more concise and
writable. One contribution of our work is bringing polymorphic
functions and type inference, found in functional programming
languages like SML and Haskell, to object-oriented programming
languages like Java in the context of writing annotations, thus
blending the benefits of two programming paradigms.
support functional program verification. In functional verification, a
program is viewed as a mathematical function that maps one program
state to another, and thus proving the correctness of a program is
essentially comparing two mathematical functions, the function
implemented by the program and its specification. Since the CleanJava
notation is based on Java expressions with extensions such as
mathematical structures like sets and sequences, its vocabulary is
limited that of Java. In this paper, we propose to make the CleanJava
language more expressive by enhancing its extension mechanism. Our
approach is to support user-defined mathematical functions, functions
introduced by the user for the purpose of writing annotations. They
not only enrich the vocabulary of CleanJava but also allow one to tune
the abstraction level of CleanJava annotations. The user-defined
mathematical functions are polymorphic---meaning that they may be
applied to values of different types---and the signatures of the
functions need not be declared. Both the signatures of user-defined
functions and the types of CleanJava expressions are inferred
statically. Polymorphic functions allow one to write generic and
reusable functions, and resulting annotations become more concise and
writable. One contribution of our work is bringing polymorphic
functions and type inference, found in functional programming
languages like SML and Haskell, to object-oriented programming
languages like Java in the context of writing annotations, thus
blending the benefits of two programming paradigms.