A Process for the Specification of Core JDK Classes

Note: This project was accomplished by MSc student Ralph Hyland is late 2009 and early 2010. Ralph's original proposal and final report are available.

  • Supervisor Dr. Joseph Kiniry
  • Subject Area programming and specification languages
  • Pre-requisite good understanding of object-oriented programming in Java, basic understanding of the Java Modeling Language (JML), contracts, and unit testing
  • Co-requisite (things you must learn along the way) writing specifications in JML, using the JML tool suite and ESC/Java2, advanced unit testing
  • Subject Coverage class specification and unit testing, static analysis
  • Project Type analysis, design, and implementation
  • Hardware/Software PC, laptop or workstation capable of running Java and Eclipse

Description

To understand complex APIs like those available for Java, (e.g., the core classes in the packages java.lang, java.io, java.util, etc.), one needs a precise description of the API's behavior. While natural language documentation, like that found in Sun Microsystems's Javadocs for JDK 5, has improved API documentation over the past ten years, such "specifications" are vague, imprecise, and error-prone.

The Java Modeling Language (JML, for short) is the de facto standard for writing precise specifications of Java programs. JML is used by many courses around the world (including here at UCD), applied at several companies, and is supported by many tools. JML is an extension of Java that permits one to write assertions, like invariants and pre- and post-conditions, about Java classes and interfaces. Various tools support using such specifications to, among other things, generate runtime assertion checks, generating Javadoc-like documentation, generating method-level unit tests, and statically checking that method implementations fulfill their specifications.

New specifications for core JDK classes (e.g., java.lang.String) are typically written "on-demand", as they are necessary for the testing and verification of new programs that exercise previously unused portions of the (very large) Java platform API. In the past, such specifications were written by experts who essentially "translated" Javadocs English into JML.

Unfortunately, such specifications are rarely useful because (a) they do not target a particular use-case (e.g., run-time checking vs. verification), (b) they are not rigorously tested in any way, and (c) they are based upon erroneous data in the first place (i.e., Javadocs).

Recently a new specification writing process has been introduced by Dr. David Cok. This process involves writing new specifications and complementary specification-centric unit tests that target a particular use-case. The purpose of this project is to evaluate and extend this process by incorporating existing available comprehensive unit tests suites.

Mandatory

  1. Review and refine knowledge of JML already gained in Dr. Kiniry's Software Engineering modules.
  2. Learn the verification-centric software engineering process (the KindSoftware Process), as specified by Dr. Kiniry.
  3. Learn the basic use of the JML compiler, unit testing with JML-jUnit, and documentation generation with jmldoc.
  4. Obtain JDK unit test suites from Classpath Project and Sun.
  5. Setup local automated nightly or triggered runtime- and static checking-based ("hybrid unit testing") testing of JDK core classes.
  6. Evaluate existing JML and ESC/Java2 JDK specifications against this test suite.
  7. Write new JML specifications and complementary test suites for at least three JDK core classes.
  8. Document and refine through experience the process by which one should write such specifications incorporating hybrid unit testing.

Discretionary

  1. Write JML specifications and complementary test suites for a core JDK package.
  2. Incorporate other static analysis tools into hybrid test suite.

Exceptional

  1. Co-author a paper with Dr. Kiniry on this specification-centric process.

Sources of information and preparatory reading

  1. The KindSoftware Coding Standard
  2. The JML tool suite
  3. The Extended Static Checker for Java, ESC/Java2
  4. Design by Contract