'Extracting' and Reasoning about the wp/sp Calculus of ESC/Java2

  • Supervisor Dr. Joseph Kiniry
  • Subject Area Theoretical Computer Science and Software Engineering
  • Pre-requisite Good knowledge of Java and a basic understanding of weakest-precondition calculi
  • Co-requisite (things you must learn along the way) Basic knowledge of PVS
  • Subject Coverage Software Engineering, Weakest Precondition Calculi, Formal Specifications, Extended Static Checking, Verification, Logical Frameworks
  • Project Type Mathematics, Refactoring an existing design
  • Hardware/Software PC, laptop or workstation capable of running Java and Eclipse

Description

To perform modular extended static checking, ESC/Java2 uses a weakest precondition/strongest postcondition calculus to derive verification conditions. While (some version of) this calculus was documented in a design document by the original ESC/Java authors in escj16c.pdf, unfortunately the calculus's realization is completely embedded in the source code of the tool. Thus, we have no "independent" specification of the calculus available, independent of the Java code.

The goal of this project is to specify this calculus "externally" to the Java code in such a way that we can (a) reason about the calculus, and (b) use the calculus to derive its implementation or drive an external engine that performs the equivalent transformation on the behalf of the main tool.

Mandatory

  1. Read and understand the original paper documenting the calculus.
  2. Review the implementation of the calculus in the ESC/Java2 source code and compare it to the documented calculus.
  3. Specify the calculus in PVS or Maude.
  4. Design an API for communication between a verification tool and the external component that will perform the rewriting.

Discretionary

  1. Coauthor, submit, and publish a paper on this work.
  2. Specify the calculus, or perform a translation of the calculus specified above, in PVS or Maude (whichever tool was not used above).
  3. Write a translation tool from the chosen specification language to the secondary language.
  4. Write a translation tool from the chosen specification language to Java.
  5. Implement and test the communication API designed in above.

Exceptional

  1. Prove that the calculus is Church-Rosser.

Sources of information and preparatory reading

  1. The JML web site
  2. The ESC/Java2 web site
  3. Download, install, and play around with the JML tool suite and ESC/Java2 to get a feel for the technology.