Gary T. Leavens

Abstract Multiple Concerns in Aspect-Oriented Language Design: A Language Engineering Approach to Balancing Benefits, with Examples (2008)

Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs (2008)

Some in the aspect-oriented community view a programming language as aspect-oriented only if it allows programmers to perfectly eliminate scattering and tangling. That is, languages that do not allow...

Steve M. Shaner, Gary T. Leavens, David A. Naumann

What we call a “higher-order method ” (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design...

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...

Organizers (2008)

John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...

This report contains the papers presented at FTfJP ’07: 9th workshop on Formal

Visitor Pattern (2008)

Gary T. Leavens, Todd D. Millstein, Single Dispatch (smalltalk, Whileloop Forloop

• Based on dynamic class of receiver only p1.equal(p2) Multiple dispatch (CLOS, Dylan, Cecil): • Based on dynamic class of many arguments equal(p1, p2) Leavens & Millstein Multiple Dispatch...

Organizers (2008)

John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...

This report contains the papers presented at FTfJP ’07: 9th workshop on Formal

Formal Aspects of Computing (2008)

Gary T. Leavens, Jeannette M. Wing, G. T. Leavens, J. M. Wing

Abstract. The interface specification of a procedure describes the procedure’s behaviour using pre- and postconditions. These pre- and postconditions are written using various functions. If some of...

Formal Aspects of Computing (2008)

Gary T. Leavens, Jeannette M. Wing, G. T. Leavens, J. M. Wing

Abstract. The interface specification of a procedure describes the procedure’s behaviour using pre- and postconditions. These pre- and postconditions are written using various functions. If some of...

Newcastle, UK (2008)

Gary T. Leavens, Michael Butler, Eric Hehner, Simon Peyton-jones, Alessandro Coglio, Cliff Jones, ...

Under consideration for publication in Formal Aspects of Computing Specification and verification challenges for sequential object-oriented programs (2008)

Gary T. Leavens, K. Rustan, M. Leino, Peter Müller

Abstract. The state of knowledge in how to specify sequential programs in object-oriented languages such as Java and C # and the state of the art in automated verification tools for such programs...

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...

Integrating Random Testing with Constraintsfor Improved Efficiency and Diversity (2008)

Yoonsik Cheon, Antonio Cortes, Martine Ceberio, Gary T. Leavens

The pre- and postcondition technique wa... (2007)

Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker

history constraint.

Formalized Data Flow Diagram Specification Language (2007)

Tim Wahls, Tim Wahls, Albert L. Baker, Albert L. Baker, Gary T. Leavens, ...

While traditional Data Flow Diagrams (DFDs) are popular, they lack the formality needed in a good specification technique. We provide an executable semantics for a subset of RTSPECS, a formalization...

Contents (2007)

Submitted to the European Conference on Object-Oriented Programming, ECOOP '93. (2007)

This report describes the design of a distributed program that searched for peaks in certain measures related to the 3x+1 problem. The searches for peaks in the number of steps taken, the maximum...

Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

object-oriented programming languages

Contents (2007)

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...

Blended Algebraic and Denotational Semantics for ADT Languages with Mutable Objects (2007)

Gary T. Leavens, Gary T. Leavens, Krishna Kishore Dhara, Krishna Kishore Dhara

data types; F.3.2 [Logics and Meanings of Programs] Semantics of Programming Languages--- algebraic approaches to semantics, denotational semantics. Submitted for publication.

Contents (2007)

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...

Specification Facets for More Precise, Focused Documentation (2007)

Gary Leavens Iowa, Gary T. Leavens, Clyde Ruby

Specification languages could aid reuse to a larger extent if they could document all important facets of software, not just functional behavior. Since a specification language designer cannot know...

Specification Facets for More Precise, Focused Documentation (2007)

Gary Leavens, Gary T. Leavens, Clyde Ruby, Clyde Ruby

Specification languages could aid reuse to a larger extent if they could document all important facets of software, not just functional behavior. Since a specification language designer cannot know...

Towards Safe Modular Extensible Objects (2007)

Chambers Leavens, Cecil Language, Gary T. Leavens, Gary T. Leavens, Craig Chambers, Craig Chambers, ...

We discuss the module system of the Cecil language, which has a flexible means of customizing views of objects. Multi-methods with invocation based on static scoping, a module system, and extension...

Département de Mathématiques et Informatique (2007)

Uperieure Ormale, N Ecole, Kim B. Bruce, Kim B. Bruce, Luca Cardelli, Luca Cardelli, ...

Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...

Aiding Self-motivation with Readings in Introductory Computing (2007)

Composition Graphs, a Foundation for Reasoning about Aspect-Oriented Composition...... 1 (2007)

Students can achieve self-motivation and a broader appreciation of computing by reading widely about computing. This paper advocates discussing self-motivation with students, and suggesting that they...

Gary T. Leavens, Curtis Clifton (editors, István Nagy

Keywords: Aspect-oriented programming, modular reasoning, alternating transition systems, composition, inter-aspect dependencies, AspectJ, aspect classification, aspect reuse, composition graphs,...

for More Practical Reasoning (2007)

Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

Keywords: Cross-type aliasing, viewpoint restriction, weak behavioral subtyping, strong behavioral subtyping, aliasing, mutation, modularity, specication, veri cation, Java language, JML language.

Preventing Cross-Type Aliasing for More Practical Reasoning (2007)

Krishna Kishore Dhara, Gary T. Leavens

Abstract. To reason about the correctness of a method when cross-type aliases are possible, one must not only consider all possible patterns of aliasing among the method’s arguments, but all...

Specification and Verification of Component-Based Systems Workshop at OOPSLA 2001 (2007)

Dimitra Giannakopoulou, Gary T. Leavens, Murali Sitaraman (editors

checkers, class invariants, correctness proofs, formal methods, model checking, programming by contract,

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

Specification and Verification of Component-Based Systems Workshop (2007)

Features | Abstract data types, classes and objects, modules, packages, polymorphism, (2007)

The associated poster summarizes results from the OOPSLA 2001 workshop on Specification and Verification of Component-Based Systems. The workshop's goal is to explore foundations for applying...

JML Reference Manual DRAFT, $Revision: 1.65 $ (2007)

cation, Java language, JML language.

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...

b (2007)

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. R. Kiniry, G. T. Leavens, ...

An overview of JML tools and applications www.jmlspecs.org

Advances and Issues in JML Java Verification Workshop 2002 January 12, 2002 Gary T. Leavens http://www.cs.iastate.edu/~leavens (2007)

Gary T. Leavens, Joint Yoonsik Cheon, Curt Clifton, Clyde Ruby, Arun Raghavan, ...

much easier to maintain than code .Rigorous semantics: can use for verification Approach .Java expressions for assertions ( la Eiffel) .Model-based specifications (Larch, VDM) Contribution .Language...

Formal Methods for Industrial Critical Systems (FMICS ’03), vol. 80 of Electronic Notes in Theoretical Computer Science, pp. 73–89, Elsevier, 2003.] (2007)

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...

G.T.: Quantified, typed events for improved separation of concerns (2007)

Hridesh Rajan, Gary T. Leavens, Hridesh Rajan

Implicit invocation and aspect-oriented languages provide related but distinct mechanisms for separation of concerns. Implicit invocation languages have explicitly announced events, which runs...

Ownership and effects for more effective reasoning about aspects (2007)

Curtis Clifton, Gary T. Leavens, James Noble, Curtis Clifton, Gary T. Leavens, James Noble

Keywords: Aspect-oriented programming, ownership, concern domain, control effects,

Following the Grammar (2007)

G.T.: Quantified, typed events for improved separation of concerns (2007)

cc✐

Hridesh Rajan, Gary T. Leavens, Hridesh Rajan, Gary T. Leavens, Hridesh Rajan

Implicit invocation and aspect-oriented languages provide related but distinct mechanisms for separation of concerns. Implicit invocation languages have explicitly announced events, which runs...

Roadmap for Enhanced Languages and Methods to Aid Verification (2006)

Leavens, Gary T., Abrial, Jean-Raymond, Batory, Don, Butler, Michael, Coglio, Alessandro, Fisler, Kathi, ...

This roadmap describes ways that researchers in four areas — speci- fication languages, program generation, correctness by construction, and programming languages — might help further the goal of...

Roadmap for Enhanced Languages and Methods to Aid Verification (2006)

Leavens, Gary T., Abrial, Jean-Raymond, Batory, Don, Butler, Michael, Coglio, Alessandro, Fisler, Kathi, ...

This roadmap describes ways that researchers in four areas — speci- fication languages, program generation, correctness by construction, and programming languages — might help further the goal of...

Roadmap for Enhanced Languages and Methods to Aid Verification (2006)

Leavens, Gary T., Abrial, Jean-Raymond, Batory, Don, Butler, Michael, Coglio, Alessandro, Fisler, Kathi, ...

This roadmap describes ways that researchers in four areas — speci- fication languages, program generation, correctness by construction, and programming languages — might help further the goal of...

Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)

Erik Poll, Patrice Chalin, David Cok, Joe Kiniry, Gary T. Leavens

Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most computer science and software...

MiniMAO1: An imperative core language for studying aspect-oriented reasoning (2006)

Behavioral subtyping is equivalent to modular reasoning for object-oriented programs (2006)

This paper describes MiniMAO1, a core aspect-oriented language. Unlike previous aspect-oriented calculi and core languages, MiniMAO1 allows around advice to change the target object of an advised...

Gary T. Leavens, David A. Naumann

Abstract. Behavioral subtyping enables modular reasoning about the functional behavior of object-oriented programs. It validates supertype abstraction, that is, modular reasoning about dynamically...

Following the Grammar (2006)

Java Modeling Language (JML), and explains how (2006)

Scheme.

Gary T. Leavens, David A. Naumann, Gary T. Leavens, David A. Naumann

This document gives a tutorial introduction to the

Abstract (2006)

Submitted for publication

Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)

Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll

Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre-...

and Modular Reasoning (2006)

Gary T. Leavens, David A. Naumann, Gary T. Leavens

Submitted for publication

Preliminary definition of core JML (2006)

Gary T. Leavens, David A. Naumann, Stan Rosenberg, Gary T. Leavens, David A. Naumann, Stan Rosenberg

Abstract: The JML specification language has evolved over a number of years and several variations/subsets have been formalized, mainly in the context of prototype systems for runtime and static...

Table of Contents (2006)

Abstract Design by Contract with JML (2006)

assertion checkers, class invariants, formal methods, programming

// @ requires x> = 0.0; (2006)

This document gives a tutorial introduction to the

Gary T. Leavens, Yoonsik Cheon, Ensures Jmldouble

This document gives a tutorial introduction to the

Computer Science Research and Writing (2006)

Roadmap for Enhanced Languages and Methods to Aid Verification (2006)

www.cs.iastate.edu/~leavens/

Gary T. Leavens, Dale Miller

This roadmap describes ways that researchers in four areas — specification languages, program generation, correctness by construction, and programming languages — might help further the goal of...

Roadmap for Enhanced Languages and Methods to Aid Verification (2006)

Gary T. Leavens, Jean-raymond Abrial, Don Batory, Michael Butler, Ro Coglio, Kathi Fisler, ...

2006 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications — languages, methodologies;

Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)

Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll

Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre-...

Modular invariants for layered object structures (2006)

Peter Müller, Arnd Poetzsch-heffter, Gary T. Leavens

Classical specification and verification techniques support invariants for individual objects whose fields are primitive values, but do not allow sound modular reasoning about invariants involving...

A contextual interpretation of undefinedness for runtime assertion checking (2005)

Gary T. Leavens, Yoonsik Cheon, Yoonsik Cheon

Java Modeling Language (JML), and explains how (2005)

Gary T. Leavens, Curtis Clifton, Brian Dorn, Copyright Gary, T. Leavens, Curtis Clifton, ...

This document is distributed under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1, or (at your option) any later version.

Java Modeling Language (JML), and explains how (2005)

This document gives a tutorial introduction to the

This document gives a tutorial introduction to the

Extending JML for modular specification and verification of multi-threaded programs (2005)

Gary T. Leavens, Curtis Clifton, Brian Dorn, Copyright Gary, T. Leavens, Curtis Clifton, ...

This document is distributed under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1, or (at your option) any later version.

Edwin Rodríguez, Matthew Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens

Abstract. The Java Modeling Language (JML) is a formal specification language for Java that allows developers to specify rich software contracts for interfaces and classes, using pre- and...

Java Modeling Language (JML), and explains how (2005)

Gary T. Leavens, Curtis Clifton, Brian Dorn, Copyright Gary, T. Leavens, Curtis Clifton, ...

This document is distributed under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1, or (at your option) any later version.

A design discipline and language features for formal modular reasoning in aspect-oriented programs (2005)

This document gives a tutorial introduction to the

Languages] Language Constructs and Features — control structures, modules, packages, procedures, functions and subroutines, advice, spectators, assistants, aspects. Submitted for publication.

Lessons from the JML Project (2005)

Gary T. Leavens, Curtis Clifton, Gary T. Leavens, Curtis Clifton

Submitted for publication

MiniMAO: Investigating the Semantics of Proceed (2005)

Extending JML for modular specification and verification of multi-threaded programs (2005)

This paper describes the semantics of MiniMAO 1 , a core aspectoriented calculus. Unlike previous aspect-oriented calculi, it allows around advice to change the target object of an advised operation...

Edwin Rodríguez, Matthew Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens

Abstract. The Java Modeling Language (JML) is a formal specification language for Java that allows developers to specify rich software contracts for interfaces and classes, using pre- and...

Gary T. Leavens, Copyright Gary, T. Leavens, Curtis Clifton, Curtis Clifton

This document is distributed under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2, or (at your option) any later version.

Example (2005)

The JML and JUnit Way of Unit Testing and its Implementation (2004)

• Writing unit test code is hard

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...

MultiJava: Design rationale, compiler implementation, and applications (2004)

Curtis Clifton, Todd Millstein, Gary T. Leavens, Craig Chambers

MultiJava is a conservative extension of the Java programming language that adds symmetric multiple dispatch and open classes. Among other benefits, multiple dispatch provides a solution to the...

MultiJava: Design rationale, compiler implementation, and applications (2004)

Curtis Clifton, Todd Millstein, Gary T. Leavens, Craig Chambers, Curtis Clifton, Todd Millstein, ...

— abstract data types, classes and objects, control structures, inheritance,

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

JML Reference Manual (2004)

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)

An overview of JML tools and applications (2004)

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...

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.

MultiJava: Design rationale, compiler implementation, and applications (2004)

Curtis Clifton, Curtis Clifton, Todd Millstein, Todd Millstein, Gary T. Leavens, Gary T. Leavens, ...

— abstract data types, classes and objects, control structures, inheritance,

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

Abstract Obliviousness, Modular Reasoning, and the Behavioral Subtyping Analogy ∗ (2003)

The obliviousness property of AspectJ conflicts with the ability to reason about an AspectJ program in a modular fashion. This makes debugging and maintenance difficult. In object-oriented...

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

ABSTRACT Parameterized Aspect Calculus: A Core Calculus for the Direct Study of Aspect-Oriented Languages (2003)

Curtis Clifton, Gary T. Leavens, Mitchell W, Curtis Clifton

Features — classes and objects Submitted for publication.

Formal definition of the parameterized aspect calculus (2003)

Curtis Clifton, Gary T. Leavens, Mitchell W, Curtis Clifton, Gary T. Leavens

This paper gives the formal definition of the parameterized aspect calculus, or ςasp. The ςasp calculus is a core calculus for the formal study of aspect-oriented programming languages. The...

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...

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...

Parameterized Aspect Calculus: A Core Calculus for the Direct Study of Aspect-Oriented Languages (2003)

Curtis Clifton, Gary T. Leavens, Mitchell Wand

Formal study of aspect-oriented languages is di#cult because current theoretical models provide a range of features that is too limited and rely on encodings using lower-level abstractions, which...

Abstract Obliviousness, Modular Reasoning, and the Behavioral Subtyping Analogy ∗ (2003)

The obliviousness property of AspectJ conflicts with the ability to reason about an AspectJ program in a modular fashion. This makes debugging and maintenance difficult. In object-oriented...

G.T.: Obliviousness, modular reasoning, and the behavioral subtyping analogy (2003)

Abstract. The obliviousness property of AspectJ-like languages conflicts with the ability to reason about programs in a modular fashion. This can make debugging and maintenance difficult. In...

Formal definition of the parameterized aspect calculus (2003)

Mitchell W, Curtis Clifton, Curtis Clifton, Gary T. Leavens, Gary T. Leavens

This paper gives the formal definition of the parameterized aspect calculus, or ςasp. The ςasp calculus is a core calculus for the formal study of aspect-oriented programming languages. The...

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)

A runtime assertion checker for the Java Modeling Language (JML (2002)

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...

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

Spectators and Assistants: (2002)

Languages] Language Constructs and Features — control structures, modules, packages, procedures, functions and subroutines,

Spectators and Assistants: (2002)

Languages] Language Constructs and Features — control structures, modules, packages, procedures, functions and subroutines,

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...

Observers and Assistants: A Proposal for Modular Aspect-Oriented Reasoning (2002)

Gary T. Leavens and Ron Cytron (editors) TR 02-06 April 2002 Aspect-oriented programming languages, formal semantics, formal methods, specification, (2002)

In general, aspect-oriented programs require a whole-program analysis to understand the semantics of a single method invocation. This property can make reasoning difficult, impeding maintenance...

Verification Theory Of, Gary T. Leavens, Ron Cytron (editors

this paper was presented at the 9th International Workshop on Foundations of ObjectOriented Languages, January 19, 2002

Equational reasoning with subtypes (2002)

Gary T. Leavens, Don Pigozzi

Abstract. Using equational logic as a specification language, we investigate the proof theory of behavioral subtyping for object-oriented abstract data types with immutable objects and deterministic...

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...

Equational Reasoning with Subtypes (2002)

Gary Leavens And, Copyright Gary, T. Leavens, Gary T. Leavens, Gary T. Leavens, Don Pigozzi, ...

data types, classes and objects; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs | Logics of programs, speci - cation techniques; F.3.2 [Logics and...

Spectators and Assistants: Enabling Modular Aspect-Oriented Reasoning (2002)

In current aspect-oriented languages, separate compilation and modular reasoning are not possible. This detracts from comprehensibility and impedes maintenance eorts. We describe language features...

1 Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction (2002)

Gregory W. Kulczycki, Murali Sitaraman, William F. Ogden, Bruce W. Weide, Gary T. Leavens, Gregory W. Kulczycki, ...

languages; D.2.4 [Software Engineering] Software/Program Verification- correctness proofs, formal methods, programming by contract, reliability; D.3.1 [Programming

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

and Techniques — Object-oriented design methods; D.2.3 [Software Engineering] Coding Tools and Techniques — Object-oriented programming; D.2.4 [Software Engineering] Software/Program Verification — Class invariants, correctness (2002)

Peter Müller, Arnd Poetzsch-heffter, Gary T. Leavens, Peter Müller, Arnd Poetzsch-heffter, Gary T. Leavens

Java language, JML language.

Alias-free parameters in C for Better Reasoning and Optimization (2001)

Medhat G. Assaad, Gary T. Leavens, Medhat G. Assaad

— control primitives, functional constructs.

Alias-free parameters in C for Better Reasoning and Optimization (2001)

Medhat G. Assaad, Medhat G. Assaad, Gary T. Leavens, Gary T. Leavens

Submitted for publication.

Preliminary design of JML (2001)

Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, Clyde Ruby, Clyde Ruby

specification techniques. Copyright c fl 1998, 1999 by Iowa State University. This document s distributed under the terms of the GNU General Public License as published by the Free Software...

Larch frequently asked questions (2001)

Spying on Components: A Runtime Verification Technique............................................................... 7 (2001)

Permission is granted for you to make copies of this FAQ for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for...

Dimitra Giannakopoulou, Gary T. Leavens, Murali Sitaraman (editors

checkers, class invariants, correctness proofs, formal methods, model checking, programming by contract,

Mutation, Aliasing, Viewpoints, Modular Reasoning, and Weak Behavioral Subtyping (2001)

Gary T. Leavens, Krishna Kishore Dhara, Krishna Kishore Dhara

invariants, logics of programs, pre- and post-conditions, specification techniques; Submitted for publication

MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java (2000)

JML: notations and tools supporting detailed design in Java (2000)

We present MultiJava, a backward-compatible extension to Java supporting open classes and symmetric multiple dispatch. Open classes allow one to add to the set of methods that an existing class...

Gary T. Leavens, K. Rustan, M. Leino, Erik Poll, Clyde Ruby, Bart Jacobs, ...

2000 ACM. Permission to make digital or hard copies of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial...

MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java (2000)

Curtis Clifton, Gary T. Leavens, Craig Chambers, Todd Millstein, Curtis Clifton, Gary T. Leavens

compilation.

Contents 1 From Executable Formal Specification to Java Property Verification...............…. (2000)

Sophia Antipolis, Sophia Drossopoulou, Susan Eisenbach, Bart Jacobs, Gary T. Leavens, I. Attali, ...

Desugaring JML Method Specifications (2000)

Arun D. Raghavan, Arun D. Raghavan, Gary T. Leavens, Gary T. Leavens

techniques; Copyright c ○ 2000, 2001 by Iowa State University. This document is distributed under the terms of the GNU General Public License as published by the Free Software Foundation; either...

MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java (2000)

Curtis Clifton, Gary T. Leavens, Craig Chambers, Todd Millstein

We present MultiJava, a backward-compatible extension to Java supporting open classes and symmetric multiple dispatch. Open classes allow one to add to the set of methods that an existing class...

Safely Creating Correct Subclasses without Seeing Superclass Code (2000)

Clyde Ruby, Clyde Ruby, Gary T. Leavens, Gary T. Leavens

A major problem for object-oriented frameworks and class libraries is how to provide enough information about a superclass, so programmers can safely create new subclasses without giving away the...

JML: notations and tools supporting detailed design in Java (2000)

Gary T. Leavens, Gary T. Leavens, Clyde Ruby, Clyde Ruby, K. Rustan, ...

JML is a notation for specifying the detailed design of Java classes and interfaces. JML's assertions are stated using a slight extension of Java's expression syntax. This should make it...

Desugaring JML Method Specifications (2000)

Arun D. Raghavan, Arun D. Raghavan, Gary T. Leavens, Gary T. Leavens

JML, which stands for "Java Modeling Language," is a behavioral interface specification language (BISL) designed to specify Java modules. JML features a great deal of syntactic sugar that...

Formal Semantics and Soundness of an Algorithm for Translating Model-based Specifications to Constraint Programs (2000)

Tim Wahls, Tim Wahls, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens

This paper presents an algorithm for executing formal specications, and a proof of the soundness of that algorithm. The algorithm executes specications written in the model-based specication language...

Concepts of Behavioral Subtyping and a Sketch of their Extension to Component-Based Systems (2000)

Gary T. Leavens, K.K. Dhara, Krishna Kishore Dhara

Object-oriented systems are able to treat objects indirectly by message passing. This allows them to manipulate objects without knowing their exact runtime type. Behavioral subtyping helps one reason...

MultiJava: Modular symmetric multiple dispatch and extensible classes for Java (2000)

Copyright Curtis Clifton, Craig Chambers, Craig Chambers, Todd Millstein, Todd Millstein, Curtis Clifton, ...

Languages] Language Classifications — object-oriented languages; D.3.3 [Programming Languages] Language Constructs and Features — abstract data types, classes and objects, control structures,...

JML: A Notation for Detailed Design (1999)

Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1999)

JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It...

ACL - Eliminating Parameter Aliasing with Dynamic Dispatch (1999)

JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...

Gary T. Leavens, Gary T. Leavens, Olga Antropova, Olga Antropova

. We have designed and prototyped a new approach for eliminating reference parameter aliases. This approach allows procedure calls with overlapping call-by-reference parameters, but guarantees that...

Enhancing the Pre- and Postcondition Technique for More Expressive Specifications (1999)

Copyright C Fl, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

. We describe enhancements to the pre- and postcondition technique that help specifications convey information more effectively. Some enhancements allow one to specify redundant information that can...

Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1999)

Copyright Gary, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...

JML: A notation for detailed design (1999)

Enhancing the pre- and postcondition technique for more expressive specifications (1999)

JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It...

Gary T. Leavens, Albert L. Baker

We describe enhancements to the pre- and postcondition technique that help specifications convey reuse contracts more effectively. Some enhancements also allow one to specify redundant information...

Formal Semantics for Structured Analysis Style Data Flow Diagram Specification Languages (1999)

Albert L. Baker, Gary T. Leavens, Gary T. Leavens, Tim Wahls, Tim Wahls

Using operational semantic techniques, we present a formal semantics for an extended variant of structured analysis style data ow diagrams. This semantics is intended to serve as a semantic...

Enhancing the pre- and postcondition technique for more expressive specifications (1999)

Copyright C, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

and Reasoning about Programs | Pre- and post-conditions, speci cation techniques.

Typeset by AMS-TEX ALGEBRAIC CHARACTERIZATION OF BEHAVIORAL SUBTYPING 1 A COMPLETE ALGEBRAIC CHARACTERIZATION OF BEHAVIORAL SUBTYPING (1999)

Gary T. Leavens, Don Pigozzi, Gary T. Leavens, Don Pigozzi

Keywords:behavioral subtype, subtyping, behavior, realization, observable equivalence, simulation, abstract data type.

Verifying Object-Oriented Programs That Use Subtypes. (1998)

Leavens, Gary T.

Object-oriented programming languages like Smalltalk-80 have a generic invocation mechanism that allows code to work on instances of many different types. In this dissertation we show how to write...

Preliminary design of JML: A behavioral interface specification language for Java (1998)

Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, Clyde Ruby, Clyde Ruby

JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...

Preliminary design of JML: A behavioral interface specification language for Java (1998)

Copyright Gary, T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...

Class-Based and Algebraic Models of Objects (1998)

Gary T. Leavens, Gary T. Leavens, Don Pigozzi, Don Pigozzi, Don Pigozzi

data types; F.3.2 [Logics and Meanings of Programs ] Semantics of Programming Languages --- algebraic approaches to semantics, denotational sematics. Submitted for publication. c fl Gary T. Leavens...

Multiple Dispatch as Dispatch on Tuples (1998)

Copyright Gary, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Todd D. Millstein, Todd D. Millstein, ...

Many popular object-oriented programming languages, such as C++, Smalltalk-80, Java, and Eiffel, do not support multiple dispatch. Yet without multiple dispatch, programmers find it difficult to...

JML: a Java Modeling Language (1998)

Protective Interface Specifications (1998)

JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...

Multiple Dispatch as Dispatch on Tuples (1998)

. The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these...

Gary Leavens, Gary T. Leavens, Todd D. Millstein, Todd D. Millstein

Many popular object-oriented programming languages, such as C++, Smalltalk-80, Java, and Eiffel, do not support multiple dispatch. Yet without multiple dispatch, programmers find it difficult to...

ACL - Eliminating Parameter Aliasing with Dynamic Dispatch (1998)

Olga Antropova, Olga Antropova, Gary T. Leavens, Gary T. Leavens

We have implemented a new method for eliminating reference parameter aliases. This method allows procedure calls with overlapping call-by-reference parameters, but at the same time guarantees that...

Programming is Writing: Why Student Programs Need to be Carefully Read (1998)

Teaching a student to write computer programs well is much like teaching a student to write English prose well. That is, although a program must be correct in every last detail, achieving correctness...

Multiple Dispatch as Dispatch on Tuples (1998)

Gary T. Leavens, Gary T. Leavens, Todd D. Millstein, Todd D. Millstein

Many popular object-oriented programming languages, such as C++, Smalltalk-80, Java, and Eiffel, do not support multiple dispatch. Yet without multiple dispatch, programmers find it difficult to...

Executing Formal Specifications with Constraint Programming (1998)

Tim Wahls, Tim Wahls, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker

We have implemented a technique for execution of formal, model-based specifications. The specifications we can execute are written at a level of abstraction that has not previously been supported in...

Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1998)

Copyright Gary, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

JML is a behavioral interface specification language tailored to Java. JML is designed to be used by working software engineers, and requires only modest mathematical training. To achieve this goal,...

Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1998)

Copyright Gary, Gary Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...

Preliminary design of JML: A behavioral interface specification language for Java (1998)

Executing formal speci cations with constraint programming (1998)

theory, Larch, Ei el, JML, ESC/Java; D.2.4 [Software Engineering] Software/Program Veri cation

Gary T. Leavens, Albert L. Baker, Tim Wahls, Tim Wahls

Keywords: Executable speci cations, constraint programming, SPECS-C++ AKL, behavioral

Executing formal speci cations with constraint programming (1998)

Gary T. Leavens, Tim Wahls, Tim Wahls, Albert L. Baker, Albert L. Baker

techniques. Submitted for publication.

Preliminary design of JML: A behavioral interface specification language for Java (1998)

Copyright Gary, T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

JML is a behavioral interface speci cation language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to veri cation and debugging. JML is designed to be used by...

Class-Based and Algebraic Models of Objects (1998)

Gary T. Leavens, Gary T. Leavens, Don Pigozzi, Don Pigozzi, Don Pigozzi

| Abstract data types; F.3.2 [Logics and Meanings of Programs] Semantics of

ACL — Eliminating Parameter Aliasing with Dynamic Dispatch (1998)

Olga Antropova, Olga Antropova, Gary T. Leavens, Gary T. Leavens

call-by-result patterns.

Preliminary design of JML: A behavioral interface specification language for Java (1998)

ACL — Eliminating Parameter Aliasing with Dynamic Dispatch (1998)

assertion checkers, class invariants, formal methods, programming

Gary T. Leavens, Gary T. Leavens, Olga Antropova, Olga Antropova

patterns.

Executing formal speci cations with constraint programming (1998)

Gary T. Leavens, Tim Wahls, Tim Wahls, Albert L. Baker, Albert L. Baker

reliability, tools; D.2.m [Software Engineering] Miscellaneous | Rapid prototyping; D.3.2 [Programming

Multiple dispatch as dispatch on tuples (1998)

Copyright Gary, T. Leavens, Gary T. Leavens, Gary T. Leavens, Todd D. Millstein, Todd D. Millstein, ...

D.3.2 [Programming Languages] Language Classifications — object-oriented languages; D.3.3 [Programming Languages] Language Constructs and Features — abstract data types, control structures,...

ABSTRACT (1998)

Gary T. Leavens, Todd D. Millstein, Gary T. Leavens

[Programming Languages] Language Classifications — object-oriented languages; D.3.3 [Programming Languages] Language Constructs and Features — abstract data types, control structures, procedures,...

Multiple dispatch as dispatch on tuples (1998)

Copyright Gary, T. Leavens, Todd Millstein, Todd Millstein, Gary T. Leavens, Gary T. Leavens, ...

D.3.2 [Programming Languages] Language Classifications — object-oriented languages; D.3.3 [Programming Languages] Language Constructs and Features — abstract data types, control structures,...

BeCecil, A core object-oriented language with block structure and multimethods: Semantics and typing (1997)

Polymorphic Type-Checking in Scheme (1997)

We present and analyze the semantics and static type system for BeCecil, a theoretical (core) language with multimethods. BeCecil is a simple and orthogonal version of object-oriented languages like...

Steven L. Jenkins, Gary T. Leavens

This paper presents a type-inference system for Scheme that is designed to be used by students in an introductory programming course. The major goal of the work is to present a type system that is...

Gary Leavens, Gary T. Leavens, Jeannette M. Wing, Jeannette M. Wing

The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these...

Enhancing the Pre- and Postcondition Technique for More Expressive Specifications (1997)

Copyright Gary, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...

We describe enhancements to the pre- and postcondition technique that help specifications convey reuse contracts more effectively. Some enhancements also allow one to specify redundant information...

Forcing Behavioral Subtyping Through Specification Inheritance (1997)

Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

data types, modules, packages; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- Pre- and post-conditions, specification techniques. c fl Copyright...

Reference Manual (1997)

Draft Revision, Gary T. Leavens

Classes], page 231 for details.) Line 8 starts the specification of the behavior of the member function largest. Line 9 gives the precondition for the member function, and line 11 the postcondition;...

Gary T. Leavens, Gary T. Leavens, Jeannette M. Wing, Jeannette M. Wing

The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these...

Gary T. Leavens, Gary T. Leavens, Jeannette M. Wing, Jeannette M. Wing

The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these...

Executing Formal Specifications with Constraint Satisfaction (1997)

Tim Wahls, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker

We have implemented an execution technique for formal specifications, which is based on constraint satisfaction techniques. These techniques allow one to execute model-based specifications written at...

Gary Leavens, Gary T. Leavens, Jeannette M. Wing, Jeannette M. Wing

The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these...

BeCecil, a Core Object-Oriented Language with Block Structure and Multimethods: Semantics and Typing (1997)

Protective interface specifications (1997)

We present and analyze the semantics and static type system for BeCecil, a theoretical (core) language with multimethods. BeCecil is a simple and orthogonal version of object-oriented languages like...

Protective interface specifications (1997)

The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these...

Abstract (1997)

Gary T. Leavens, Clyde Ruby, Gary T. Leavens, Clyde Ruby

F.3.1 [Logics and Meaning of Programs] Specifying and verifying and reasoning about programs | Assertions, invariants, pre- and post-conditions, speci cation techniques.

Protective interface specifications (1997)

The Hopkins Objects Group (1996)

Abstract The interface specification of a procedure describes the procedure's behavior using pre- and postconditions. These pre- and postconditions are written using various functions. If some...

Kim Bruce, Luca Cardelli, Gary T. Leavens, Benjamin Pierce

Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...

An overview of Larch/C++: Behavioral specifications for C++ modules (1996)

Edited Haim Kilov, William Harvey, Gary T. Leavens, Gary T. Leavens

redundancy, behavioral subtype, informality, tunable formality. 1993 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications--- Languages; F.3.1 [Logics and Meaning of Programs]...

Formal Semantics for Structured Analysis Style Data Flow Diagram Specification Languages (1996)

Gary T. Leavens, Gary T. Leavens, Tim Wahls, Tim Wahls, Albert L. Baker, Albert L. Baker

Using operational semantic techniques, we present a formal semantics for an extended variant of structured analysis style data flow diagrams. This semantics is intended to serve as a semantic...

BeCecil, A Core Object-Oriented Language with Block Structure and Multimethods: Semantics and Typing (1996)

Craig Chambers, Craig Chambers, Gary T. Leavens, Gary T. Leavens

We present and analyze the semantics and static type system for BeCecil, a theoretical (core) language with multimethods. BeCecil is a simple and orthogonal version of object-oriented languages like...

An Operational Semantics of Firing Rules for Structured Analysis Style Data Flow Diagrams (1996)

Gary T. Leavens, Gary T. Leavens, Tim Wahls, Tim Wahls, Albert L. Baker, Albert L. Baker, ...

Using operational semantic techniques, an extended variant of structured analysis style data flow diagrams is given a formal semantics. This semantics allows one to describe both how information is...

The Behavior-Realization Adjunction and Generalized Homomorphic Relations (1996)

Gary Leavens, Gary T. Leavens, Don Pigozzi, Don Pigozzi

data types; F.3.2 [Logics and Meanings of Programs ] Semantics of Programming Languages --- algebraic approaches to semantics; F.3.2 [Mathematical Logic and Formal Languages ] Mathematical Logic ---...

A Physical Example For Teaching Curried Functions (1996)

Protection from the Underspecified (1996)

Curried functions are an important topic in Computing courses that teach functional programming, including courses that study programming languages. Good motivating examples for teaching curried...

An Overview of Larch/C++: Behavioral Specifications for C++ Modules (1996)

Underspecification is a good way to deal with partial functions in specification and reasoning. However, when underspecification is used, implementations may unintentionally be forced to depend on...

Forcing Behavioral Subtyping Through Specification Inheritance (1996)

This chapter is an overview of the behavioral interface specification language Larch/C++. Besides describing the specification language in general and giving some examples, the features of Larch/C++...

Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

data types, modules, packages; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- Pre- and post-conditions; F.3.1 [Logics and Meanings of Programs]...

Protection from the Underspecified (1996)

Gary T. Leavens, Gary T. Leavens, Jeannette M. Wing, Jeannette M. Wing

Underspecification is a good way to deal with partial functions in specification and reasoning. However, when underspecification is used, implementations may unintentionally be forced to depend on...

An Overview of Larch/C++: Behavioral Specifications for C++ Modules (1996)

An Overview of Larch/C++: Behavioral Specifications for C++ Modules (1996)

An overview is presented of the behavioral interface specification language Larch/C++. The features of Larch/C++ used to specify the behavior of C++ functions and classes, including subclasses, are...

An Overview of Larch/C++: Behavioral Specifications for C++ Modules (1996)

An overview is presented of the behavioral interface specification language Larch/C++. The features of Larch/C++ used to specify the behavior of C++ functions and classes, including subclasses, are...

Edited Haim Kilov, William Harvey, Gary Leavens, Gary T. Leavens

An overview is presented of the behavioral interface specification language Larch/C++. The features of Larch/C++ used to specify the behavior of C++ functions and classes, including subclasses, are...

Polymorphic Type-Checking in Scheme (1996)

Steven L. Jenkins, Steven L. Jenkins, Gary T. Leavens, Gary T. Leavens

This paper presents a type-inference system for Scheme that is designed to be used by students in an introductory programming course. The major goal of the work is to present a type system that is...

An Overview of Larch/C++: Behavioral Specifications for C++ Modules (1996)

Forcing Behavioral Subtyping Through Specification Inheritance (1996)

An overview is presented of the behavioral interface specification language Larch/C++. The features of Larch/C++ used to specify the behavior of C++ functions and classes, including subclasses, are...

Krishna Kishore, Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

data types, modules, packages; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- Pre- and post-conditions; F.3.1 [Logics and Meanings of Programs]...

An Overview of Larch/C++: Behavioral Specifications for C++ Modules (1996)

Edited Haim Kilov, William Harvey, Gary T. Leavens, Gary T. Leavens

An overview is presented of the behavioral interface specification language Larch/C++. The features of Larch/C++ used to specify the behavior of C++ functions and classes, including subclasses, are...

Typeset by AMS-TEX ALGEBRAIC CHARACTERIZATION OF BEHAVIORAL SUBTYPING 1 AN EXACT ALGEBRAIC CHARACTERIZATION OF BEHAVIORAL SUBTYPING (1996)

Gary T. Leavens, Don Pigozzi, Gary T. Leavens, Don Pigozzi

Keywords:behavioral subtype, subtyping, behavior, realization, observable equivalence, simulation, abstract data type.

Polymorphic type-checking in Scheme (1996)

Steven L. Jenkins, Steven L. Jenkins, Gary T. Leavens, Gary T. Leavens

data types, data types and structures. D.3.4 [Programming Languages] Processors-preprocessors.

An overview of Larch/C++: Behavioral specifications for C++ modules (1996)

An overview of Larch/C++: Behavioral specifications for C++ modules (1996)

inheritance, example, checkable redundancy, behavioral subtype, informality, tunable formality. 1993 CR Categories: D.2.1 [Software Engineering] Requirements/Speci cations | Languages; F.3.1 [Logics...

Edited Haim Kilov, William Harvey, Gary T. Leavens, Gary T. Leavens

behavioral subtype, informality, tunable formality.

An overview of Larch/C++: Behavioral specifications for C++ modules (1996)

Forcing behavioral subtyping through specification inheritance (1996)

checkable redundancy, behavioral subtype, informality, tunable formality.

Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any...

Weak behavioral subtyping for types with mutable objects (1995)

Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

types; F.3.1 [Logics and Meaning of Programs] Specifying and verifying and reasoning about programs--- logics of programs; F.3.2 [Logics and Meanings of Programs] Semantics of Programming...

Typechecking and Modules for Multi-Methods (1995)

An Exact Algebraic Characterization Of Behavioral Subtyping (1995)

Two major obstacles hindering the wider acceptance of multi-methods are concerns over the lack of encapsulation and modularity and the absence of static typechecking in existing multi-method-based...

Gary Leavens And, Gary T. Leavens, Don Pigozzi

. A model theory for correct behavioral subtyping for abstract data types (with immutable objects) is developed within the framework of the behavior-realization adjunction. To allow for incomplete...

Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, Jonathan Eifrig, Scott F. Smith, Valery Trifonov, ...

Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...

Foundations of Object-Oriented Languages (1995)

Kim Bruce, Luca Cardelli, Gary T. Leavens, Benjamin Pierce

This paper offers a comprehensive description of the problems arising from typing binary methods, and collects and contrasts diverse views and solutions. It summarizes the current debate on the...

Nd Workshop, Gary T. Leavens

A report on the workshop Foundations of ObjectOriented Languages, Paris, July 1994. 1 Introduction In Paris on July 1--2 1994, researchers gathered at the second workshop of a series of NSF and...

An Exact Algebraic Characterization of Behavioral Subtyping (1995)

Gary T. Leavens, Benjamin Pierce, Giuseppe Castagna, Kim Bruce, Kim Bruce, ...

data types, modules, packages; F.3.1 [Logics and Meanings of Programs ] Specifying and Verifying and Reasoning about Programs --- logics of programs; F.3.2 [Logics and Meanings of Programs ] Studies...

Gary T. Leavens, Gary T. Leavens, Don Pigozzi, Don Pigozzi

data types; F.3.2 [Logics and Meanings of Programs ] Semantics of Programming Languages --- algebraic approaches to semantics; F.3.2 [Mathematical Logic and Formal Languages ] Mathematical Logic ---...

Typechecking and Modules for Multi-Methods (1995)

Kim Bruce, Kim Bruce, Luca Cardelli, Luca Cardelli, Gary T. Leavens, Gary T. Leavens, ...

data types, modules, packages; F.3.2 [Logics and Meanings of Programs] Studies of Program Constructs --- type structure. To appear in Theory and Practice of Object Systems. Copyright c fl assigned to...

Gary T. Leavens, Craig Chambers, Craig Chambers

Two major obstacles hindering the wider acceptance of multi-methods are concerns over the lack of encapsulation and modularity and the absence of static typechecking in existing multi-method-based...

On binary methods (1995)

Kim Bruce, Luca Cardelli Y, Gary T. Leavens, Benjamin Pierce K

Giving types to binary methods causes signi cant problems for object-oriented language designers and programmers. This paper o ers a comprehensive description of the problems arising from typing...

Typechecking and Modules for Multi-Methods (1995)

Craig Chambers, Craig Chambers, Gary T. Leavens, Gary T. Leavens

Two major obstacles hindering the wider acceptance of multi-methods are concerns over the lack of encapsulation and modularity and the absence of static typechecking in existing multi-method-based...

modular specification, and modular verification for applicative object-oriented programs (1994)

Gary T. Leavens, Gary T. Leavens, William E. Weihl, William E. Weihl

and reasoning about programs--- logics of programs, pre- and post-conditions, specification

The direct execution of specs-c++: A model-based specification language for c++ classes (1994)

Albert L. Baker, Albert L. Baker, Gary T. Leavens, Gary T. Leavens, Tim Wahls, Tim Wahls, ...

Engineering] Miscellaneous--- rapid prototyping

Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs (1994)

Gary T. Leavens, Gary T. Leavens, William E. Weihl, William E. Weihl

data types, procedures, functions, and subroutines; F.3.1 [Logics and Meanings of Programs ] Specifying and verifying and reasoning about programs --- logics of programs, pre- and post-conditions,...

Type Checking and Modules for Multi-Methods (1994)

Type Checking and Modules for Multi-Methods (1994)

Two major obstacles hindering the wider acceptance of multi-methods are concerns over the lack of encapsulation and modularity and the absence of static typechecking in existing multi-method-based...

Chambers Leavens, Gary T. Leavens, Craig Chambers, Craig Chambers

ing with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications...

Blended Algebraic and Denotational Semantics for ADT Languages with Mutable Objects (1994)

Gary T. Leavens, Gary T. Leavens, Krishna Kishore Dhara, Krishna Kishore Dhara

Data Types with Mutable Objects (extended abstract)". Keywords: algebraic semantics, algebraic models, denotational semantics, abstract data type, objects, mutation, model theory, simulation...

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....

Fields in Physics are like Curried Functions or Physics for Functional Programmers (1994)

Towards Safe Modular Extensible Objects (1994)

Good motivating examples for teaching the utility of curried functions can be taken from Physics. The curried function perspective can also be used to help functional programmers understand fields in...

Chambers Leavens, Cecil Language, Gary T. Leavens, Gary T. Leavens, Craig Chambers, Craig Chambers, ...

We discuss the module system of the Cecil language, which has a flexible means of customizing views of objects. Multi-methods with invocation based on static scoping, a module system, and extension...

Inheritance of Interface Specifications (1994)

Extend Ed, Gary T. Leavens, Gary T. Leavens

) Gary T. Leavens TR #93-23 September 1993 Keywords: specification, inheritance, subtype, subclass, modularity, objectoriented, abstract data type. 1992 CR Categories: D.2.1 [Software Engineering ]...

Aiding Self-motivation with Readings in Introductory Computing (1994)

The Larch/Smalltalk Interface Specification Language (1994)

Students can achieve self-motivation and a broader appreciation of computing by reading widely about computing. This paper advocates discussing self-motivation with students, and suggesting that they...

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....

Inheritance of Interface Specifications (1994)

Extend Ed, Gary T. Leavens, Gary T. Leavens

) Gary T. Leavens TR #93-23 September 1993 Keywords: specification, inheritance, subtype, subclass, modularity, objectoriented, abstract data type. 1992 CR Categories: D.2.1 [Software Engineering ]...

Weak Behavioral Subtyping for Types with Mutable Objects (1994)

Krishna Kishore Dhara, Krishna Kishore Dhara, Gary T. Leavens, Gary T. Leavens

This paper studies the question of when one abstract data type (ADT) is a behavioral subtype of another, and proposes a model-theoretic notion of weak beh...

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...

Foundations of Object-Oriented Languages - 2nd Workshop report (1994)

Giuseppe Castagna, Gary T. Leavens, Gary T. Leavens

data types, modules, packages; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- logics of programs; F.3.2 [Logics and Meanings of Programs] Semantics...

The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes (1994)

Albert L. Baker, Gary T. Leavens, Tim Wahls, Tim Wahls

Executable specification languages may be the key to more widespread use of formal methods in software production. However, the expressiveness of executable specification languages is typically much...

Typechecking and Modules for Multi-Methods (1994)

Chambers Leavens, Gary T. Leavens, Craig Chambers, Craig Chambers

Two major obstacles preventing the wider acceptance of multi-methods are concerns over the lack of encapsulation and modularity and the lack of static typechecking in existing multi-method-based...

Introduction to the Literature On Semantics (1994)

An executable semantics for a formalized data flow diagram specification language (1993)

Albert L. Baker, Albert L. Baker, Gary T. Leavens, Gary T. Leavens, Tim Wahls, Tim Wahls, ...

Engineering] Miscellaneous--- rapid prototyping

An Operational Semantics of Firing Rules for Structured Analysis Style Data Flow Diagrams (1993)

Gary Leavens, Gary T. Leavens, Tim Wahls, Tim Wahls, Albert L. Baker, Albert L. Baker, ...

Using operational semantic techniques, an extended variant of structured analysis style data flow diagrams is given a formal semantics. This semantics allows one to describe both how information is...

Introduction to the Literature On Programming Language Design (1993)