Checking JML Specification Soundness using ESC/Java2

Note: Initial work on this project was accomplished by fourth year student Connor Gallagher (report). The prototype of the implementation is part of ESC/Java2.

  • Supervisor Dr. Joseph Kiniry
  • Subject Area Software Engineering with Applied Theoretical Computer Science
  • Pre-requisites Good knowledge of Java and logic
  • Co-requisites (things you must learn along the way) knowledge of predicate calculus, wp calculus, and program verification
  • Subject Coverage Formal Specifications, Extended Static Checking, Verification, Logic
  • Project Type Design and Implementation
  • Hardware/Software PC, laptop or workstation capable of running Java and Eclipse

Description

JML is the de facto standard behavioral specification language for Java. Many powerful research tools understand JML, including ESC/Java2. ESC/Java2 is the world's most advanced extended static checker. It automatically checks that a Java program conforms to its JML formal specification. This magic is accomplished with the use of a rich object logic, a wp calculus for Java and JML, and an automated first-order theorem prover. Unfortunately, but unsurprisingly, people are prone to writing incorrect programs and specifications. One of the trickiest issues encountered by ESC/Java2 users (of which there are hundreds around the world) is detecting and resolving inconsistencies in their specifications. For example, if at one place in your program you say that a reference can be null and in another place you indirectly mention that it cannot be null, this is an inconsistency, and therefore your specification is not logically sound. Over the years we have developed a process by which one can determine if an inconsistency exists and, if so, where it is. Unfortunately, this is a manual, labor-intensive process. Happily, it is quite regular, and therefore can be automated. The goal of this project is to automate and extend this process, thereby adding the most requested (and terrifically important) functionality to ESC/Java3. The results of this work will be part of a new release of the tool and a research publication with Dr. Kiniry.

Mandatory Goals

  1. Build experience with specification and verification with JML and ESC/Java2.
  2. Identification of key strategies for specification refinement.
  3. Identification of strategies for detecting soundness problems.
  4. Design for new ESC/Java3 functionality that automatically realizes the strategies practiced "by-hand" today for 2) and 3).
  5. Implementation of design.
  6. Testing of implementation on small case studies.
  7. Release to the world with a new version of ESC/Java3!
  8. Write, submit, and publish a paper on the results.

Discretionary Goals

  1. Examining all existing specifications of core Java classes (much of the java.lang and java.util packages) for inconsistencies would be an excellent case study that would be a wonderful service to the community and would constitute the foundation for an excellent conference research paper.

Exceptional Goals

  1. The development of a formal model of program refinement that includes specification refinement and soundness would be outstanding.

Sources of Information and Preparatory Reading

  1. The JML web site
  2. The ESC/Java2 web site
  3. Read the two recent papers available via the JML web page: "An overview of JML tools and applications" and "JML: notations and tools supporting detailed design in Java".
  4. Read "ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2" available via the ESC/Java2 web site.
  5. Download, install, and play around with the JML tool suite and ESC/Java2 to get a feel for the technology.