An Aspect-Based Approach to Checking Design Constraints at Run-time (2009)
Carmen Avila, Steve Roach, Cuahtemoc Munoz, Neith Estrada, Valeria Fierro, Jessica Romo, ...
JML Reference Manual DRAFT, $Revision: 1.220 $ $Date: 2008/01/08 22:43:42 $ (2008)
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, ...
Permission is granted for you to make copies of this manual for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for...
Integrating Random Testing with Constraints for Improved Efficiency and Diversity (2008)
Yoonsik Cheon, Antonio Cortes, Martine Ceberio, Gary T. Leavens, Yoonsik Cheon, Antonio Cortes, ...
methods, programming by contract; D.2.5 [Software Engineering] Testing and Debugging — testing tools (e.g., data generators, coverage testing); D.3.2 [Programming Languages] Language...
Carmen Avila, Guillermo Flores, Yoonsik Cheon
interfaces, object-oriented design methods; D.2.4 [Software Engineering] Software/Program Verification⎯assertion checkers, class invariants, formal methods, programming by contract; D.2.6 [Software...
Integrating Random Testing with Constraintsfor Improved Efficiency and Diversity (2008)
Yoonsik Cheon, Antonio Cortes, Martine Ceberio, Gary T. Leavens
An Aspect-Based Approach to Checking Design Constraints at Run-time (2008)
Yoonsik Cheon, Carmen Avila, Steve Roach, Cuahtemoc Munoz, Neith Estrada, Valeria Fierro, ...
checkers, class invariants, formal methods, programming by contract; D.3.2 [Programming Languages] Language
Carmen Avila, Guillermo Flores, Yoonsik Cheon
interfaces, object-oriented design methods; D.2.4 [Software Engineering] Software/Program
Little Smalltalk, Gary T. Leavens, Yoonsik Cheon
1991 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications--- Languages; F.3.1 [Log-ics and Meaning of Programs] Specifying and verifying and reasoning about programs--- pre- and...
Little Smalltalk, Gary T. Leavens, Yoonsik Cheon
1991 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications--- Languages; F.3.1 [Log-ics and Meaning of Programs] Specifying and verifying and reasoning about programs--- pre- and...
Tree-based Algorithm to Find the (2007)
Th Value, Yoonsik Cheon, Yoonsik Cheon, Johnny Wong, Johnny Wong
In this paper, we study distributed algorithms for finding the k-th value in the decentralized systems. First we consider the case of circular configuration of processors where no processor knows the...
A Simple and Practical Approach to Unit (2007)
Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens, Gary T. Leavens
invariants, pre- and post-conditions, specication techniques. Submitted for publication
JML Reference Manual DRAFT, $Revision: 1.65 $ (2007)
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, ...
Permission is granted for you to make copies of this manual for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for...
L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. R. Kiniry, G. T. Leavens, ...
An overview of JML tools and applications www.jmlspecs.org
Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, ...
Abstract. The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a...
Architectural Assertions: Checking Architectural Constraints at Run-Time (2007)
Hyotaeg Jung, Eric Wong, Yoonsik Cheon, Hyotaeg Jung, ...
class invariants, formal methods; programming by contract; D.2.11 [Software Engineering] Software
Abstract—An interface specification language such as JML provides a means to document precisely the behavior of program modules such as Java classes, and it is being adopted by industry. However,...
In evolutionary testing of an object-oriented program, the search objective is to find a sequence of method calls that can successfully produce a test object of an interesting state. This is...
Random test data generation for Java classes annotated with JML specifications (2007)
Abstract — The hidden states of objects create a barrier to designing and generating test data automatically. For example, the state of an object has to be established indirectly through a sequence...
Abstraction in Assertion-Based Test Oracles (2007)
about Programs — Assertions, invariants, pre- and post-conditions, specification techniques.
Java Modeling Language (JML), and explains how (2006)
Gary T. Leavens, Yoonsik Cheon
This document gives a tutorial introduction to the
A formal specification in JML of the Java security package (2006)
Poonam Agarwal, Yoonsik Cheon, Patricia J. Teller, Poonam Agarwal, ...
Verifying and Reasoning about Programs — Assertions, invariants, pre- and post-conditions, specification
Abstract Design by Contract with JML (2006)
Gary T. Leavens, Yoonsik Cheon
This document gives a tutorial introduction to the
// @ requires x> = 0.0; (2006)
Gary T. Leavens, Yoonsik Cheon, Ensures Jmldouble
This document gives a tutorial introduction to the
and Meanings of Programs] Specifying and Verifying and Reasoning about Programs⎯assertions, (2006)
Angelica B. Perez, Yoonsik Cheon, Ann Q. Gates
invariants, pre- and post-conditions, specification techniques.
Java Modeling Language (JML), and explains how (2005)
Gary T. Leavens, Yoonsik Cheon
This document gives a tutorial introduction to the
Java Modeling Language (JML), and explains how (2005)
Gary T. Leavens, Yoonsik Cheon
This document gives a tutorial introduction to the
Java Modeling Language (JML), and explains how (2005)
Gary T. Leavens, Yoonsik Cheon
This document gives a tutorial introduction to the
A Fitness Function for Modular Evolutionary Testing of (2005)
formal methods, programming by contract; D.2.5 [Software Engineering] Testing and Debugging — testing tools (e.g., data generators, coverage testing); D.3.2 [Programming Languages] Language...
Specifying and Checking Method Call Sequences of Java Programs (2005)
Yoonsik Cheon, Yoonsik Cheon, Ashaveena Perum, Ashaveena Perum
invariants, mechanical verifications, pre- and post-conditions, specification techniques;
Method Call Sequences in JML (2005)
Yoonsik Cheon, Ashaveena Perum
Abstract — In a pre and postconditions style specification, it is difficult to specify allowed sequences of method calls, often called protocols. However, the protocols are essential properties of...
A complete automation of unit testing for Java programs (2005)
Yoonsik Cheon, Yoonsik Cheon, Myoung Yee Kim, Myoung Yee Kim, Ashaveena Perum, Ashaveena Perum
Verifying and Reasoning about Programs — Assertions, invariants, pre- and post-conditions, specification techniques.
The JML and JUnit Way of Unit Testing and its Implementation (2004)
Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens, Gary T. Leavens
Submitted for publication
A thought on specification reflection (2004)
Yoonsik Cheon, Yoshiki Hayashi, Gary T. Leavens
In programming languages, reflection is the ability to discover and manipulate, at runtime, information about program entities, such as objects. We present our thoughts on extending the concept of...
Leavens JML Framed! 3 Behavioral Interface Specification (2004)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Rustan Leino, Bart Jacobs, Erik Poll, ...
Behavioral interface specification language, tailored to Java • Records detailed designs • Pre- and postconditions, invariants,... • Synthesizes ideas in sequential specification
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, ...
this document. The specification of the method largest is given on lines 7 through 15. Line 7 says that this is a public, normal behavior specification. JML permits several di#erent specifications...
Design by Contract with JML (2004)
Gary T. Leavens, Yoonsik Cheon
This document gives a tutorial introduction to the Java Modeling Language (JML), and explains how JML can be used as a powerful design by contract (DBC) tool for Java. JML is a formal behavioral...
An overview of JML tools and applications (2004)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Davidr. Cok, Michael D. Ernst, Joseph R. Kiniry, ...
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...
How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification (2004)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok
Specifications that are used in detailed design and in the documentation of existing code are primarily written and read by programmers.
A runtime assertion checker for the Java Modeling Language / (2003)
The Java Modeling Language (JML) is a formal behavioral interface specification language (BISL) for Java. JML has many advances including specification-only declarations, specifications of...
JML Reference Manual DRAFT, $Revision: 1.29 $ (2003)
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby
Permission is granted for you to make copies of this manual for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for...
Model Variables: Cleanly Supporting (2003)
Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, Stephen Edwards, Stephen Edwards D
Techniques — modules and interfaces, object-oriented design methods; D.2.4
How the design of JML accommodates both runtime assertion checking and formal verification (2003)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok, Gary T. Leavens, ...
Techniques — modules and interfaces, object-oriented design methods; D.2.4
An Overview of JML Tools and Applications (2003)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, ...
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...
An overview of JML tools and applications (2003)
Lilian Burdy, Yoonsik Cheon, Joe Kiniry, ...
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...
An overview of JML tools and applications (2003)
Www Jmlspecs Org, Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, ...
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...
Model Variables: Cleanly Supporting Abstraction in Design by Contact (2003)
Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, Murali Sitaraman, Stephen Edwards, Stephen Edwards
In design by contract (DBC), assertions are typically written using program variables and query methods. This technique does not allow specifiers to write modeloriented specifications for interfaces...
An overview of jml tools and applications (2003)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T, ...
original version is available at www.springerlink.com
An overview of JML tools and applications (2003)
Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, ...
1 Introduction JML [25, 26], which stands for "Java Modeling Language", is useful for specifying detailed designs of Java classes and interfaces. JML is a behavioral interface specification...
Design by contract with JML (2003)
Gary T. Leavens, Yoonsik Cheon
This document gives a tutorial introduction to the Java Modeling Language (JML), and explains how JML can be used as a powerful design by contract (DBC) tool for Java. JML is a formal behavioral...
A runtime assertion checker for the Java Modeling Language (JML (2002)
Yoonsik Cheon, Gary T. Leavens, Yoonsik Cheon, Gary T. Leavens
Programs] Specifying and Verifying and Reasoning about Programs — Assertions, invariants, pre- and post-conditions, specification techniques. Submitted for publication
A Simple and Practical Approach to Unit Testing: The JML and JUnit Way (2002)
Yoonsik Cheon, Gary T. Leavens, Yoonsik Cheon, Gary T. Leavens
Abstract. Writing unit test code is labor-intensive, hence it is often not done as an integral part of programming. However, unit testing is a practical approach to increasing the correctness and...
A Runtime Assertion Checker for the Java Modeling Language (JML) (2002)
Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens, Gary T. Leavens
Debugging is made difficult by the need to precisely describe what each piece of the software is supposed to do, and to write code to defend modules against the errors of other modules; if this is...
A Simple and Practical Approach to Unit Testing: The JML and JUnit Way (2002)
Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens, Gary T. Leavens
invariants, pre- and post-conditions, specification techniques. Submitted for publication
A Specifier's Dilemma, An Abstraction Problem in Interface Specifications (2000)
ions in Interface Specifications Yoonsik Cheon and Heung-Nam Kim Software Engineering Department ETRI Computer & Software Technology Laboratories 161 Kajung-dong, Yusong-ku, Taejon 305-350 Rep....
The Larch/Smalltalk Interface Specification Language (1994)
About Programs Assertions, Specification Techniques, Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens, Gary T. Leavens
Object-oriented programming languages, such as Smalltalk, help one to build reusable program modules. The reuse of program modules requires adequate documentation --- formal or informal....
The Larch/Smalltalk Interface Specification Language (1994)
About Programs Assertions, Specification Techniques, Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens, Gary T. Leavens
Object-oriented programming languages, such as Smalltalk, help one to build reusable program modules. The reuse of program modules requires adequate documentation --- formal or informal....
A Quick Overview of Larch/C++ (1994)
Yoonsik Cheon, Yoonsik Cheon, Gary T. Leavens, Gary T. Leavens
This paper gives a quick overview of Larch/C++ , an interface specification language for C++ . Through examples, we explain declarations, function specifications, class specifications, and template...
Tree-based Algorithm to Find the k-th Value in Distributed Systems (1994)
Yoonsik Cheon, Yoonsik Cheon, Johnny Wong, Johnny Wong
In this paper, we study distributed algorithms for finding the k-th value in the decentralized systems. First we consider the case of circular configuration of processors where no processor knows the...
Preliminary design of Larch/C (1992)
Gary T. Leavens, Gary T. Leavens, Yoonsik Cheon, Yoonsik Cheon
of Programs] Specifying and verifying and reasoning about programs--- Assertions, invariants, pre- and
Larch/Smalltalk :--a specification language for Smalltalk /--by Yoonsik Cheon. (1991)
Typescript (photocopy)
Larch/Smalltalk : a specification language for Smalltalk / (1991)
Abstract: "Larch/Smalltalk is a Larch interface specification language for Smalltalk with subtype relations. As a Larch-style language it benefits from two-tiered approach to specifications;...
Larch/Smalltalk: A specification language for Smalltalk (1991)
Yoonsik Cheon, Yoonsik Cheon, Yoonsik Cheon
type checking. 1991 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications--- Languages; D.3.3 [Programming Languages] Language Constructs--- Abstract data types, procedures,...
Larch/Smalltalk: A Specification Language for Smalltalk (1991)
: : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : ix CHAPTER 1. INTRODUCTION : : : : : : : : : : : : : : : : : : : : : : 1 1.1 Background : : : : : : : : : : : : : : : : : : : : :...