Vol 5 No.1

The CleanJava Language for Functional Program Verification

ABSTRACT Unlike Hoare-style program verification, functional program verification supports forward reasoning by viewing a program as a mathematical function from one program state to another and proving its correctness by essentially comparing two mathematical functions, the function computed by the program and its specification. Since it requires a minimal mathematical background and reflects the way that programmers reason about the correctness of a program informally, it can be taught and practiced effectively. However, there is no formal notation supporting the functional program verification. In this article, we describe a formal notation for writing functional program specifications for Java programs. The notation, called CleanJava, is based on the Java expression syntax and is extended with a mathematical toolkit consisting of sets and sequences. The vocabulary of CleanJava can also be enriched by introducing user-specified definitions such as user-defined mathematical functions and specification-only methods. We believe that CleanJava is a good notation for writing functional specifications and expect it to promote the use of functional program verifications by being able to specify a wide range of Java programs.

Authors
Cesar Yeep
  • Organization : Department of Computer Science, University of Texas at El Paso, El Paso, Texas (U.S.A.)
  • Email : ceyeep@miners.utep.edu
Read More
Melisa Vela
  • Organization : Department of Computer Science, University of Texas at El Paso, El Paso, Texas (U.S.A.)
  • Email : smvelaloya@miners.utep.edu
Read More
Yoonsik Cheon
  • Organization : Department of Computer Science, University of Texas at El Paso, El Paso, Texas (U.S.A.)
  • Email : ycheon@utep.edu
Read More