Specification Language Design and Support Tools

Larch-style Languages

My research has focused on the design and implementation of specification languages and related tools. My earlier accomplishment in this area is designing the first Larch-style interface specification language for an object-oriented programming language called Larch/Smalltalk. The implementation of Larch/Smalltalk included a graphical user interface, integrated with the ParcPlace Smalltalk system. Larch/Smalltalk made several contributions to specification language design. It was the first object-oriented formal specification language in the Larch style. It features a clear separation of the notions of type and class. Types in Larch/Smalltalk are the unit of abstraction for specifications, and specify the protocols of objects. A type can be implemented either by a single Smalltalk class, or by several classes. Behavioral subtyping organizes types according to behavioral relationships. The language also supports specification inheritance and generic polymorphism, in addition to subtype polymorphism, at the level of types. An article on Larch/Smalltalk was published in the ACM Transactions on Software Engineering and Methodology, one of the most prestigious journals in the field (Cheon and Leavens, 1994a).

Another earlier accomplishment is the design of the formal specification language Larch/C++. I was a major collaborator in this effort. Larch/C++ uses several ideas from Larch/Smalltalk in the context of a C++. I developed the original parser, preprocessor, and reference manual for Larch/C++. I also co-authored two papers about Larch/C++; the paper "Preliminary Design of Larch/C++" was presented at the First International Workshop on Larch (Leavens and Cheon, 1992), and a tutorial "A Quick Overview of Larch/C++" was published in a peer-reviewed journal, Journal of Object-Oriented Programming (Cheon and Leavens, 1994b).

  1. Gary T. Leavens and Yoonsik Cheon. Preliminary Design of Larch/C++, Proceedings of the First International Workshop on Larch, Workshops in Computer Science, pages 159-184. Springer-Verlag. N.Y., July 1992.
  2. Yoonsik Cheon and Gary T. Leavens. The Larch/Smalltalk Interface Specification Language. ACM Transactions on Software Engineering and Methodology, 3(3):221-253, July 1994.
  3. Yoonsik Cheon and Gary T. Leavens. A Quick Overview of Larch/C++. Journal of Object-Oriented Programming, 7(6):39-49, October 1994.

The Java Modeling Language

My recent accomplishment is the contributions that I made to the Java Modeling Language (JML), an interface specification language for the Java programming language. As part of my Ph.D. dissertation research I developed a runtime assertion checking compiler (jmlc) for JML. The contributions of my work on the runtime assertion checker are not just in the software, however. I has made significant and important contributions to the design of JML and its semantics, for example, distinction between static and instance invariants, semantics of specification inheritance, and privacy issues in specifications. The most significant contributions of my dissertation work include (1) supporting abstraction in run-time assertion checking, (2) systematic support for handling undefinedness in assertions, and (3) substantial support for specification inheritance. I have written roughly 70,000 source lines for the JML tools (including code, documentation, specifications, test cases, and makefiles).

My publications, especially on JML have both been significant and had a far-reaching impact. This can be seen from the number of citations of these publications. For example, my paper (joint with Burdy, Cok, and others) on JML tools has been cited (according to Google Scholar) 344 times. My paper on unit testing (with Leavens) has been cited 145 times, and my dissertation has been cited 145 times. Furthermore, a popular college textbook on programming languages (Tucker and Noonans, Programming Languages, Principles and Paradigms, second edition, McGraw-Hill, 2007) includes sections devoted to JML, based largely on my dissertation work.

  1. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An Overview of JML Tools and Applications. International Journal on Software Tools for Technology Transfer, 7(3):212-232, June, 2005.
  2. Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, and Stephen Edwards. Model Variables: Cleanly Supporting Abstraction in Design By Contract. Software.Practice and Experience, 35(6):583.599, May, 2005.
  3. Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification. Science of Computer Programming, 55(1-3):185-208, March 2005.
  4. Yoonsik Cheon. A Runtime Assertion Checker for the Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University, Ames, IA, April 2003. The author's Ph.D. dissertation
  5. Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In Boris Magnusson (ed.), ECOOP 2002 . Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 2002, Proceedings. Volume 2374 of Lecture Notes in Computer Science, pages 231-255. Springer-Verlag, 2002.

UTJML: Extending and Revitalizing JML

My most recent accomplishments include several extensions to the JML language. With a graduate student, Ashaveena Perumandla, I introduced the notion of protocol contracts to JML (Cheon and Perumandla, 2007; refer to the project website). In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, that we referred to as protocols. However, protocols are essential properties of reusable object-oriented classes and application frameworks. We made an extension to JML to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and postconditions and to specify them in a regular expression-like notation. We defined the semantics of our extension formally and used it as a foundation for extending the JML tools to support protocol contracts. A graduate student, Carlos Rubio, and I recently proposed an approach for formally specifying access control assumptions of a Java program module and enforcing them at run-time. We called such an assumption or assertion an access control contract. For this, we introduced two new built-in JML language constructs and defined their semantics by translating them into runtime checking code. Our approach will contribute to providing a foundation for formally reasoning about security properties of Java programs and facilitate practicing the "security by design" principle.

My current work focuses on re-developing the JML tools by enhancing JML's tool infrastructure. The goal is to update the JML language and its tool support to reflect recent language changes in Java, e.g., generics, and to make JML's software infrastructure more extensible so that it can be used as a research platform for Java-based formal methods.

My recent and current work in the design and implementation of specification languages and related tools has been supported by the following two NSF research grants.

Last modified: $Id: speclang.html,v 1.5 2009/03/06 10:07:56 cheon Exp $