Functional Verification of Class Invariants in CleanJava

In a Cleanroom-style functional program verification, a program is viewed as a mathematical function from one program state to another, and a verification is done by comparing two functions, the implemented and the expected behaviors of a program. The technique requires a minimal mathematical background and supports forward reasoning, but it doesn\u27t support assertions such as class invariants. However, assertions such as class invariants are not only a practical programming tool but also play a key role in the correctness proof of a program by specifying conditions and constraints that an object has to satisfy and thus defining valid states of an object. We suggest a way to integrate the notion of a class invariant in a functional program verification by using CleanJava as a specification notation and a verification framework. CleanJava is a formal annotation language for Java to support a Cleanroom-style functional program verification. We propose a small extension to CleanJava to specify a class invariant and also to its proof logic to verify the invariant. Our extension closely reflects the way programmers specify and reason about the correctness of a program informally. It allows one to use a class invariant in the framework of a Cleanroom-style functional specification and verification