Specification Language Design and Support Tools

Larch-style Languages

Dr. Cheon's research has focused on the design and implementation of specification languages and related tools. His 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++. Dr. Cheon was a major collaborator in this effort. Larch/C++ uses several ideas from Larch/Smalltalk in the context of a C++. He developed the original parser, preprocessor, and reference manual for Larch/C++. He 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

Dr. Cheon's recent accomplishment is the contributions that he made to the Java Modeling Language (JML), an interface specification language for the Java programming language. As part of his Ph.D. dissertation research he developed a runtime assertion checking compiler (jmlc) for JML. The contributions of his work on the runtime assertion checker are not just in the software, however. he 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 his 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. he have written roughly 70,000 source lines for the JML tools (including code, documentation, specifications, test cases, and makefiles).

Dr. Cheon's 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, his paper (joint with Burdy, Cok, and others) on JML tools has been cited (according to Google Scholar) more than 1000 times. His paper on unit testing (with Leavens) has been cited more than 300 times, and his dissertation has been cited more than 300 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 his dissertation work.

  1. Yoonsik Cheon and Gary T. Leavens. A Contextual Interpretation of Undefinedness for Runtime Assertion Checking. In AADEBUG 2005, Proceedings of the Sixth International Symposium on Automated and Analysis-Driven Debugging, Monterey, California, September 19--21, 2005, pages 149-157. ACM Press, September 2005. [PDF]
  2. 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.
  3. 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.
  4. 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.
  5. 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
  6. 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.

JML Reloaded: Extending and Revitalizing JML

Dr. Cheon's most recent accomplishments include several extensions to the JML language. With a graduate student, Ashaveena Perumandla, he introduced the notion of protocol contracts to JML (Cheon and Perumandla, 2007). In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, that they call protocols. However, protocols are essential properties of reusable object-oriented classes and application frameworks. They 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. They 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 Dr. Cheon recently proposed an approach for formally specifying access control assumptions of a Java program module and enforcing them at run-time. They called such an assumption or assertion an access control contract. For this, they introduced two new built-in JML language constructs and defined their semantics by translating them into runtime checking code. Their approach will contribute to providing a foundation for formally reasoning about security properties of Java programs and facilitate practicing the "security by design" principle.

Dr. Cheon's 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 (Sarcar and Cheon, 2010).

  1. Amritam Sarcar and Yoonsik Cheon. A New Eclipse-Based JML Compiler Built Using AST Merging, Second World Congress on Software Engineering (WCSE 2010), December 19-20, 2010, Wuhan, China, pages 287-292, IEEE Computer Society. [DOI: 10.1109/WCSE.2010.92]
  2. Yoonsik Cheon and Ashaveena Perumandla. Specifying and Checking Method Call Sequences of Java Programs. Software Quality Journal, 15(1):7-25, March 2007. [DOI: 10.1007/s11219-006-9001-4]
  3. Angelica B. Perez, Yoonsik Cheon, and Ann Q. Gates. Canica: An IDE for the Java Modeling Language. In Proceedings of the 10th IASTED International Conference on Software Engineering and Applications, November 13-15, 2006, Dallas, TX, USA, pages 32-37. [PDF]
  4. Yoonsik Cheon and Ashaveena Perumandla. Specifying and Checking Method Call Sequences in JML. Proceedings of the 2005 International Conference on Software Engineering Research and Practice (SERP '05), Las Vegas, Nevada, June 27-29, 2005, pages 511-516, 2005. [PDF]

Dr. Cheon's 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.7 2019/08/17 19:29:20 cheon Exp $