CleanJava: Functional Program Verification for Java

Initially supported by NSF under Grant No. DUE-0837567, the goals of this project is to develop practical verification techniques suitable for teaching in undergraduate computer science courses and to integrating program verification to the undergraduate computer science curriculum. The mathematics to achieve these goals are sets and functions, rather than first-order predicate logic as taught in the standard computer science curriculum. An annotation notation called CleanJava incorporating recent advances in specification languages has been developed to document programs as functions from input values to output values [Cheon, Vela and Yeep 2012] [Vela and Cheon 2013]. A functional verification approach supporting a natural, intuitive, forward reasoning has been extended for modular verification of object-oriented programs [Cheon 2010] [Avila and Cheon 2012]. A formal correctness proof of code containing loops such as while loops typically uses the technique of proof-by-induction, and often the most difficult part of carrying out an inductive proof is formulating a correct induction hypothesis, a specification for a loop statement. An incorrect induction hypothesis will surely fail the proof. We developed a systematic way for identifying specifications of loop statements [Barua and Cheon 2013] [Barua and Cheon 2015]. The key idea of our approach is to categorize and document common patterns of loop statements along with their specifications [Barua and Cheon 2014] [Barua and Cheon 2018]. This is based on our observation that similarly-structured loops frequently have similarly-structured specifications. Thus, a catalog of code and specification patterns can be used as a good reference for finding and formulating a specification of a loop statement. We believe our approach is applicable to other verification techniques such as Hoare logic using pre- and post-conditions. We also developed lightweight tools for teaching and learning functional specification and verification, such as an extensible checker for the CleanJava annotation language [Yeep and Cheon 2013]. An incremental integration to the curriculum was achieved by first delivering an experimental course on program verification and then, using this experience as a guide, introducing problem-based learning modules to programming and software engineering courses in the undergraduate curriculum. Our recent work includes an application of loop patterns to code refactoring [Rahad, Cao and Cheon 2017].

  1. Aditi Barua and Yoonsik Cheon. Patterns for Systematic Derivation of Loop Specifications. Proceedings of the 2018 International Conference on Software Engineering Research & Practice, Las Vegas, Nevada, pages 229-235, July 30 - August 2, 2018, pages 229-235. [PDF]
  2. Khandoker Rahad, Zejing Cao, and Yoonsik Cheon, A Thought on Refactoring Java Loops Using Java 8 Streams, Technical Report 17-44, Department of Computer Science, University of Texas at El Paso, El Paso, TX, June 2017. [PDF]
  3. Aditi Barua and Yoonsik Cheon, A Systematic Derivation of Loop Specifications Using Patterns, Technical Report 15-90, Department of Computer Science, University of Texas at El Paso, El Paso, TX, December 2015. [PDF]
  4. Aditi Barua and Yoonsik Cheon, Finding Specifications of While Statements Using Patterns, New Trends in Networking, Computing, E-learning, Systems Sciences, and Engineering, Lecture Notes in Electrical Engineering, Volume 312, November 2014, pages 5381-588, Springer. [DOI: 10.1007/978-3-319-06764-3_75]
  5. Aditi Barua and Yoonsik Cheon, A Catalog of While Loop Specification Patterns, Technical Report 14-65, Department of Computer Science, University of Texas at El Paso, El Paso, TX, September 2014. [PDF]
  6. Aditi Barua and Yoonsik Cheon, Finding Specifications of While Statements Using Patterns, International Joint Conferences on Computer, Information, and Systems Sciences, and Engineering, December 12-14, 2013, Springer. [PDF]
  7. Yoonsik Cheon and Carmen Avila, Constructing Verifiably Correct Java Programs Using OCL and CleanJava, International Conference on Software Engineering Research and Practice, Las Vegas, Nevada, July 22-25, 2013. pages 231-237, [PDF]
  8. Melisa Vela and Yoonsik Cheon, Enhancing the Expressiveness of the CleanJava Language, Technical Report 13-33, Department of Computer Science, University of Texas at El Paso, El Paso, TX, June 2013. [PDF]
  9. Cesar Yeep and Yoonsik Cheon, CJC: An Extensible Checker for the CleanJava Annotation Language, Technical Report 13-29, Department of Computer Science, University of Texas at El Paso, El Paso, TX, May 2013. [PDF]
  10. Yoonsik Cheon, Cesar Yeep, and Melisa Vela, The CleanJava Language for Functional Program Verification, International Journal of Software Engineering, 5(1):47-68, January 2012. [PDF]
  11. Carmen Avila and Yoonsik Cheon, Functional Verification of Class Invariants in CleanJava, Innovations and Advances in Computer, Information, and Systems Sciences, and Engineering, Lecture Notes in Electrical Engineering, volume 152, Springer-Verlag, August 2012, pages 1067-1076. [DOI: 10.1007/978-1-4614-3535-8_88]

Last modified: $Id: cleanjava.html,v 1.1 2019/08/17 05:54:06 cheon Exp $