Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Research Directed by Gary T. Leavens
A roadmap for research related to verified software is found in
TR06-21.
The ACL approach to preventing aliasing from repeated parameters
is described in
TR98-08a
and the C/ACL compiler is described in
TR01-11.
Ownership applied to specifications is the topic of several papers.
TR02-02a
(an expansion of
TR01-03)
describes an application of Peter Müller's
dissertation work on modular specification of frame properties
to JML.
This is also the basis for the work on modular invariants.
Specification of superclasses to allow work on subclasses is the topic of
TR #00-05
with
Clyde Ruby;
it describes a technique for reasoning about the correctness of subclasses.
The execution of specifications in the context of the language SPECS-C++
is the subject of
TR
#00-02,
TR
#97-12a, and
TR #94-02b
with
Tim Wahls.
Various specification enhancements found in
Larch/C++
are described in
TR #97-19.
Inheritance of specifications in an object-oriented context
is discussed in a
WIDL paper.
This topic was further developed in an
ICSE 1996 paper with Krishna Kishore Dhara (see below).
Yoonsik Cheon,
Yoshiki Hayashi, and Gary T. Leavens.
A Thought on Specification Reflection.
Department of Computer Science, Iowa State University, TR #03-16,
December 2003.
[abstract][postscript][PDF]
Medhat G. Assaad and Gary T. Leavens. Alias-free parameters in
C for Better Reasoning and Optimization.
Department of Computer Science, Iowa State University,
TR #01-11, November 2001.
[abstract][postscript][PDF]
Tim Wahls and Gary T. Leavens. Formal Semantics of an Algorithm
for Translating Model-based Specifications to Concurrent Constraint
Programs. Proceedings of the 16th ACM Symposium on Applied
Computing, Las Vegas, Nevada USA, March 11-14, 2001, pp. 567-575.
Clyde Ruby
and Gary T. Leavens.
Safely Creating Correct Subclasses without Seeing Superclass Code.
In OOPSLA 2000
Conference Proceedings, pages 208-228. Volume 35, number
10 of ACM SIGPLAN
Notices, October 2000.
Also Department of Computer Science, Iowa State University,
TR #00-05d, April 2000, revised April, June, July 2000.
[abstract][postscript][PDF]
Tim Wahls, Gary T. Leavens, and Albert L. Baker. Executing Formal
Specifications with Concurrent Constraint Programming.
Automated Software Engineering,
7(4):315-343, December, 2000.
Also Department of Computer Science, Iowa State
University, TR #97-12c, August 1997, revised June 1998, May, July 2000. [abstract][postscript]
Tim Wahls and Gary T. Leavens.
Formal Semantics and Soundness of an Algorithm
for Translating Model-based Specifications to Concurrent Constraint Programs.
Department of Computer Science, Iowa State
University, TR #00-02a, March 2000, revised August 2000. [abstract][postscript]
Gary T. Leavens and Olga Antropova. ACL -- Eliminating Parameter
Aliasing with Dynamic Dispatch. Department of Computer Science, Iowa
State University, TR #98-08a, July 1998, revised February 1999. [abstract][postscript]
Hua Zhong. LSL Traits for using Z with
Larch. Department of Computer Science, Iowa State University, TR #97-22, December 1997. [abstract][postscript]
Gary T. Leavens and Albert L. Baker.
Enhancing the Pre- and Postcondition Technique
for More Expressive Specifications.
In Jeannette M. Wing, James Woodcock, and Jim Davies (editors).
FM'99 -- Formal Methods: World Congress on Formal Methods in Development
of Computer Systems, Toulouse, France, September 1999,
pages 1087--1106.
Volume 1709 of
Lecture Notes in Computer Science,
Springer-Verlag, 1999.
Also: Department of Computer Science, Iowa State University,
TR #97-19b, September 1997, revised February, June 1999.
Gary T. Leavens and Clyde Ruby.
Specification Facets for More Precise, Focused Documentation. In the Proceedings of the
Eighth Annual Workshop on Software Reuse (WISR8), Columbus Ohio, March 1997.
Also Department of Computer Science, Iowa State University, TR #97-04, January 1997. [abstract][postscript]
Gary T. Leavens and Jeannette
M. Wing. Protective Interface Specifications.
Formal Aspects of Computing, 10:59-75, 1998.
An earlier version appears in Michel Bidoit and Max Dauchet (editors), TAPSOFT '97: Theory
and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille,
France, pages 520-534. Volume 1214 of Lecture Notes in Computer Science,
Springer-Verlag, 1997.
Tim Wahls, Albert L. Baker, and Gary T.
Leavens. The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++
Classes. Department of Computer Science, Iowa State University, TR #94-02b, February 1994,
revised November 1994. [abstract][postscript]
Gary T. Leavens. Inheritance of Interface Specifications (Extended Abstract). In Proceedings
of the Workshop on Interface Definition Languages, J. M. Wing, editor, pages
129-138. Volume 29, number 8, of ACM SIGPLAN
Notices, August 1994. (Also Department of Computer Science, Iowa State
University, TR #93-23, September 1993. [abstract][postscript])
Gary T. Leavens and Yoonsik
Cheon. Overview and Specification of the Built-in Types in Little Smalltalk.
Department of Computer Science, Iowa State University, TR #91-22a, October 1991, revised
February 1994. [abstract][postscript]
Dennis de Champeaux, Pierre America, Derek Coleman, Roger Duke, Doug Lea, and Gary T.
Leavens. Formal Techniques for OO Software Development. In OOPSLA '91 Proceedings, pages
166-170. Volume 26, number 11 of ACM SIGPLAN
Notices, November 1991.
JML is a behavioral interface specification language
tailored to the specification of
Java modules.
It combines the approaches of Eiffel and
Larch,
with some elements of the
refinement calculus.
Its home page is
Yoonsik Cheon is the main designer of Larch/Smalltalk.
The current beta release of the Larch/Smalltalk system and some papers are available by
anonymous ftp from ftp.cs.iastate.edu in directory pub/larchSmalltalk.
The following paper gives the idea of designing Larch/CORBA, a behavioral interface
specification language tailored to OMG's IDL.
Gary T. Leavens and Yoonsik
Cheon. Extending CORBA IDL to Specify Behavior with Larch. In OOPSLA '93 Workshop Proceedings:
Specification of Behavioral Semantics in OO Information Modeling, pages 77-80.
(Also Department of Computer Science, Iowa State University, TR #93-20, August 1993. [abstract][text file])
More useful is the master's thesis of Gowri Sankar Sivaprasad, which gives a design of
Larch/CORBA.
Gowri Sankar Sivaprasad. Larch/CORBA: Specifying the Behavior of CORBA-IDL Interfaces.
Department of Computer Science, Iowa State University, TR #95-27a, December 1995, revised
December 1995. [abstract][postscript]
The following is recent work by Don Pigozzi,
Krishna Kishore Dhara and myself on model theory of behavior for ADTs. It is
used to study subtyping in
TR96-15.
Gary T. Leavens and Don Pigozzi. The
Behavior-Realization Adjunction and Generalized Homomorphic Relations. Theoretical Computer Science,
177:183-216, 1997.
A slightly extended version is Department of Computer Science, Iowa State University, TR
#94-18b, September 1994, revised September 1994, July 1996. [abstract][postscript]
Gary T. Leavens and Krishna Kishore Dhara. Blended Algebraic and Denotational Semantics
for ADT Languages with Mutable Objects. Department of Computer Science, Iowa State
University, TR #93-21b, September 1993, revised March, September 1994. [abstract][postscript]
An overview that ties together the ideas of supertype abstraction, behavioral subtyping, and specification inheritance is found in
TR#06-20b with David Naumann.
A presentation of these ideas in the context of JML is found in TR#06-22.
Work with Krishna Kishore Dhara on subtyping concerns types with mutable objects
is listed in this subsection. The most recent work with Dhara is TR
#01-02, which has a good explanation of the ideas.
More detailed is his
dissertation.
A shorter introduction to the idea of behavioral subtyping that may be
more accessible is the ICSE 1996 paper (which appears with a correction as
TR #95-20c).
This paper describes the idea of specification inheritance and how it relates to behavioral subtyping. Its ideas were embodied in
Larch/C++ and
JML.
Also, note that TR #94-21b
makes the following older TRs obsolete: TR #92-36 and TR #92-35. The work
described in this part does not (yet) describe a specification language or a verification
logic. Kishore's master's thesis can be had by requesting it by e-mail, but it is
summarized in TR #92-36.
Gary T. Leavens and David A. Naumann.
Behavioral Subtyping, Specification Inheritance, and Modular Reasoning.
Department of Computer Science, Iowa State University,
TR #06-20b, July 2006, revised August, September 2006.
[abstract][postscript][PDF]
Krishna Kishore Dhara and Gary T. Leavens.
Preventing Cross-Type Aliasing for More Practical Reasoning.
Department of Computer Science, Iowa State University,
TR #01-02a, March 2001, revised November 2001.
[abstract][postscript][PDF]
Krishna Kishore Dhara. Behavioral Subtyping in Object-Oriented Languages. Department of
Computer Science, Iowa State University, TR #97-09, May 1997. [abstract][postscript] (117
pages).
Krishna Kishore Dhara and Gary T. Leavens. Forcing Behavioral Subtyping Through
Specification Inheritance. In Proceedings 18th International Conference on Software
Engineering, Berlin, Germany, pages 258-267. IEEE,
1996.
An extended and slightly revised version is Department of Computer Science, Iowa State
University, TR #95-20c, August 1995, revised August and December 1995, March 1997. [abstract][postscript]
Krishna Kishore Dhara and Gary T. Leavens. Weak Behavioral Subtyping for Types with
Mutable Objects. In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical
Foundations of Programming Semantics, Eleventh Annual Conference, Preliminary
Proceedings, pages 269-290.
The final version appears in S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical
Foundations of Programming Semantics, Eleventh Annual Conference. Volume 1 of Electronic Notes in Theoretical Computer
Science, Elsevier, 1995.
The IEEE Software and OOPSLA/ECOOP '90
papers are short summaries of this work. The MFPS paper with Don
Pigozzi is also fairly short, and extends the results to higher types;
it isolates the key mathematical idea. A development of this
mathematical idea, which gives both a necessary and sufficient
model-theoretic criterion for correct behavioral subtyping is found in
TR96-15.
The proof theory is studied in
TR02-07.
Gary T. Leavens and Don Pigozzi.
Equational Reasoning with Subtypes.
Department of Computer Science, Iowa State University, TR
#02-07, July 2002. [abstract][postscript][PDF]
Gary T. Leavens and Don Pigozzi.
A Complete Algebraic Characterization of Behavioral Subtyping.
Acta
Informatica 36:617-663, 2000.
Gary T. Leavens and William E. Weihl. Specification and Verification of Object-Oriented Programs Using Supertype
Abstraction. Acta
Informatica 32(8):705-778, November 1995.
A longer version of this paper is Gary T. Leavens and William E. Weihl. Subtyping, Modular
Specification, and Modular Verification for Applicative Object-Oriented Programs.
Department of Computer Science, Iowa State University, TR #92-28d, September 1992, revised
September and October 1993, and January and September 1994. [abstract][postscript]
Gary T. Leavens and Don Pigozzi.
Typed Homomorphic Relations Extended with Subtypes. In Stephen Brookes, editor, Mathematical
Foundations of Programming Semantics '91, pages 144-167. Volume 598 of Lecture Notes in Computer Science.
Springer-Verlag, 1992.
[SpringerLink]
Gary T. Leavens, Modular Specification and Verification of Object-Oriented Programs. IEEE
Software, 8(4):72-80, July, 1991.
Gary T. Leavens and William E. Weihl. Reasoning about Object-Oriented Programs that use Subtypes (extended
abstract). In OOPSLAECOOP '90
Proceedings, pages 212-223 (Volume 25, number 10 of ACM SIGPLAN Notices, October 1990).
Gary T. Leavens. Modular Verification of Object-Oriented Programs with Subtypes.
Department of Computer Science, Iowa State University, TR #90-09, July 1990. [abstract][postscript]
Gary T. Leavens, Verifying Object-Oriented Programs that use Subtypes. Massachusetts
Institute of Technology, Laboratory for Computer Science, Technical Report TR-439,
February 1989.
The last report mentioned above, MIT/LCS/TR-439, is my Ph.D. dissertation. To get it,
check your library, or write to Publications, Laboratory for Computer Science,
Massachusetts Institute of Technology, 545 Technology Sq., Cambridge, MA 02139. Their
phone number is (617)253-5894. The cost was $16.00 US. But you probably don't need to do
that, as the thesis was reworked in a different framework in ISU TR #90-09. The Acta
Informatica paper is a summary of the thesis work; TR #92-28d contains
that paper and additional omitted details.
The first of the papers below, makes the second obsolete.
Gary T. Leavens, Tim Wahls, and Albert L. Baker. Formal Semantics
for Structured Analysis Style Data Flow Diagram Specification Languages.
In ACM SAC'99 -- 1999 ACM Symposium on Applied Computing,
San Antonio, February/March, 1999, pages 526--532.
Gary T. Leavens, Tim Wahls, Albert L. Baker, and Kari Lyle. An
Operational Semantics of Firing Rules for Structured Analysis Style Data Flow Diagrams.
Department of Computer Science, Iowa State University, TR #93-28d, December 1993, revised
December 1993, September 1994, June 1996, July 1996. [abstract][postscript]
Tim Wahls, Albert L. Baker, and Gary T.
Leavens, An Executable Semantics for a Formalized Data Flow Diagram Specification
Language. Department of Computer Science, Iowa State University, TR #93-27, November 1993.
[abstract][postscript]
Giuseppe Castagna and Gary T. Leavens. Foundations of Object-Oriented Languages: 2nd
Workshop report. Department of Computer Science, Iowa State University, TR #94-22,
November 1994. [abstract][postscript]
Curtis Clifton,
Todd Millstein,
Gary T. Leavens, and
Craig Chambers.
MultiJava: Design Rationale, Compiler Implementation, and Applications.
ACM TOPLAS,
Volume 28, number 3 (May 2006), pages 517-575.
Also Department of Computer Science, Iowa State University, TR #04-01b,
January 2004, revised December 2004.
[abstract][PDF][PostScript]
Curtis Clifton,
Gary T. Leavens, Craig Chambers, and Todd Millstein.
MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java.
In OOPSLA 2000
Conference Proceedings, pages 130-145. Volume 35, number
10 of ACM SIGPLAN
Notices, October 2000.
Also Department of Computer Science, Iowa State University,
TR #00-06a, April 2000, July 2000.
[abstract][postscript].
Gary T. Leavens and
Curtis Clifton.
A Type Notation for Scheme.
Department of Computer Science, Iowa State University,
TR #05-03, February 2005.
[abstract][PDF][postscript]
Jianbing Chen.
Dynamic Semantics and Type-checking of Tuple.
Department of Computer Science, Iowa State University, TR #98-10,
December 1998.
[abstract][postscript].
Gary T. Leavens and Todd D. Millstein.
Multiple Dispatch as Dispatch on Tuples. In OOPSLA '98
Proceedings, pages 374-387 (Volume 33, number 10 of ACM SIGPLAN Notices
October 1998).
Also Department of Computer Science, Iowa State University, TR #98-03b, April 1998,
Revised May 1998, July 1998.
[abstract][postscript].
Craig Chambers and
Gary T. Leavens. BeCecil, A Core Object-Oriented Language with Block Structure and
Multimethods: Semantics and Typing. Presented at the The Fourth International
Workshop on Foundations of Object-Oriented Languages FOOL 4, Paris, France.
An extended and slightly revised version is Department of Computer Science, Iowa State
University, TR #96-17a, December 1996, revised April 1997. [abstract][postscript (101 pages)].
The main body
and just the
appendix sections are also available.
Steven Jenkins and Gary
T. Leavens. Polymorphic Type-Checking in Scheme. Computer Languages, 22(4):
215-223, 1996.
Also Department of Computer Science, Iowa State University, TR95-21a, August 1995, revised
May 1996. [abstract][postscript]
Craig Chambers
and Gary T. Leavens. Towards Safe Modular Extensible Objects. Department of Computer
Science, Iowa State University, TR #94-17a, August 1994. [abstract][postscript]
Craig Chambers
and Gary T. Leavens. Typechecking and Modules for Multi-Methods. In OOPSLA '94 Conference Proceedings,
pages 1--15. Volume 29, number 10 of ACM
SIGPLAN Notices, October 1994.
A longer version (with formal proofs) is Department of Computer Science, Iowa State
University, TR #94-03a, March 1994, revised August 1994. [abstract][postscript]
Gary T. Leavens. Introduction to the Literature on Semantics. Department of Computer
Science, Iowa State University, TR #94-15, August 1994. [abstract][postscript][PDF]
Gary T. Leavens. Introduction to the Literature On Programming Language Design.
Department of Computer Science, Iowa State University, TR #93-01b, January 1993, revised
January 1994 and February 1996. [abstract][postscript]
Gary T. Leavens, Introduction to the Literature on Object-Oriented Design, Programming,
and Languages. OOPS Messenger, 2(4):40-53, October 1991.
Barbara Liskov, Mark Day,
Maurice Herlihy, Paul Johnson, Gary T. Leavens (editor), Robert Scheifler, and William Weihl. Argus
Reference Manual. Massachusetts Institute of Technology, Laboratory for Computer Science,
Technical Report TR-400, October 1987. [postscipt]
Gary T. Leavens.
Following the Grammar.
Department of Computer Science, Iowa State University, TR #05-02a,
February 2005, revised January 2006.
[abstract][PDF][postscript]
Gary T. Leavens. Aiding Self-motivation with Readings in Introductory Computing. Mathematics and Computer Education,
29(2):124-133, 1995.
Albert L. Baker, David Fernandez-Baca, and Gary T. Leavens.
Course Specifications for New Introductory Courses: Computer Science 227X and 228X.
Department of Computer Science, Iowa State University, TR #92-09, April 1992. [abstract][postscript]
Gary T. Leavens. A Distributed Search Program for the 3x+1 problem. Department of
Computer Science, Iowa State University, TR #89-22, November 1989. [abstract][postscript]
Kristina P. Boysen and Gary T. Leavens.
Automatically generating consistent graphical user interfaces
using a parser generator.
Department of Computer Science, Iowa State University,
TR #04-07a, August 2004, revised November 2005.
[abstract][PDF]
Gary T. Leavens. Fields in Physics are like Curried Functions, or Physics for Functional
Programmers. Department of Computer Science, Iowa State University, TR #94-06b, April
1994, revised May 1994. [abstract][postscript]
Although it might violate the copyright laws, if you don't have a published paper in
your library, you can probably get some version of it as an Iowa State University (ISU)
Computer Science TR. (This is not to encourage you to violate the copyright law, however.)
All ISU CS TRs, including many old versions, should be available by the following means.
Use ftp to connect to ftp.cs.iastate.edu, login as user anonymous,
with your e-mail address as the password. The TRs are in the directory pub/techreports with subdirectory TR90-09
holding TR 90-09, etc. (Omit any letter code. For example, TR93-18a is in directory TR93-18.)