Go to the first, previous, next, last section, table of contents.
- [America87]
-
Pierre America.
Inheritance and Subtyping in a Parallel Object-Oriented Language.
In Jean Bezivin and others (eds.),
ECOOP '87, European Conference on Object-Oriented Programming,
Paris, France.
Lecture Notes in Computer Science, Vol. 276
(Springer-Verlag, NY), pages 234-242.
- [ANSI95]
-
Woking Paper for Draft Proposed International Standard
for Information Systems -- Programming Language C++.
CBEMA, 1250 Eye Street NW, Suite 200, Washington DC 20005, April 28, 1995.
(Obtained by anonymous ftp to research.att.com, directory dist/c++std/WP.)
- [Back88]
-
R. J. R. Back.
A calculus of refinements for program derivations.
Acta Informatica, 25(6):593-624, August 1988.
- [Back-vonWright89a]
-
R. J. R. Back and J. von Wright.
Refinement Calculus, Part I: Sequential Nondeterministic Programs.
In J. W. de Bakker, et al, (eds.),
Stepwise Refinement of Distributed Systems,
Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands,
May/June 1989, pages 42-66.
Volume 430 of Lecure Notes Computer Science,
Spring-Verlag, 1989.
- [Baumgartner-Russo95]
-
Gerald Baumgartner and Vincent F. Russo.
Signatures: A Language Extension for Improving Type Abstraction
and Subtype Polymorphism in C++.
Software--Practice & Experience,
25(8):863-889, August 1995.
- [Borgida-etal95]
-
Alex Borgida, John Mylopoulos, and Raymond Reiter.
On the Frame Problem in Procedure Specifications.
IEEE Transactions on Software Engineering,
21(10):785-798, October 1995.
- [Chalin95]
-
Patrice Chalin. On the Language Design and Semantic Foundation of LCL,
a Larch/C Interface Specification Language. PhD thesis, Computer
Science Department, Concordia University, October 1995.
Also Technical Report CU/DCS TR 95-12,
which can be obtained from the URL
`ftp://ftp.cs.concordia.ca/pub/chalin/tr.ps.Z'.
- [Chalin-etal96]
-
Patrice Chalin, Peter Grogono, and T. Radhakrishnan.
Identification of and solutions to shortcomings of LCL, a Larch/C interface
specification language.
In Marie-Claude Gaudel and James Woodcock (eds.),
FME'96: Industrial Benefit and
Advances in Formal Methods, pages 385-404.
Volume 1051 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
See also CU/DCS TR 95-04, which can be obtained from the URL
`ftp://ftp.cs.concordia.ca/pub/chalin/CU-DCS-TR-95-04.ps.Z'.
- [Chen89]
-
Jolly Chen.
The Larch/Generic Interface Language.
Bachelor's thesis,
Massachusetts Institute of Technology, EECS department,
May, 1989.
(Available from John Guttag guttag@lcs.mit.edu.)
- [Cheon-Leavens94],
-
Yoonsik Cheon and Gary T. Leavens.
A Quick Overview of Larch/C++.
Journal of Object-Oriented Programming,
7(6):39-49, October 1994.
- [Dhara-Leavens94b]
-
Krishna Kishore Dhara and Gary T. Leavens.
Weak Behavioral Subtyping for Types with Mutable Objects.
In S. Brookes and M. Main and A. Melton and M. Mislove (eds.),
Mathematical Foundations of Programming Semantics,
Eleventh Annual Conference,
`http://www.elsevier.nl/locate/entcs/volume1.html'.
Volume 1 of Electronic Notes in Computer Science,
Elsevier, 1995.
- [Dhara-Leavens96]
-
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 version is
Department of Computer Science, Iowa State University,
TR #95-20b, December 1995,
which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.Z'.
- [Dhara97]
-
Krishna Kishore Dhara.
Behavioral Subtyping in Object-Oriented Languages.
Ph.D. Thesis, Department of Computer Science, Iowa State University.
Technical Report TR #97-09, May 1997.
Available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR97-09/TR.ps.gz'.
- [Dijkstra76]
-
Edsger W. Dijkstra.
A Discipline of Programming
(Prentice-Hall, Englewood Cliffs, N.J., 1976).
- [Edwards-etal94]
-
Stephen H. Edwards, Wayne D. Heym, Timothy J. Long, Murali Sitaraman,
and Bruce W. Weide.
Part II: Specifying Components in RESOLVE.
ACM SIGSOFT Software Engineering Notes,
19(4):29-39 (Oct. 1994).
- [Ellis-Stroustrup90]
-
M. A. Ellis and B. Stroustrup.
The Annotated C++ Reference Manual
(Addison-Wesley Publishing Co., Reading, Mass., 1990).
- [Ernst-etal91]
-
G. W. Ernst, R. J. Hookway, J. A. Menegay, and W. F. Ofgen.
Modular Verification of Ada Generics.
Computer Languages,
16(3/4):259-280 (1991).
- [Evans96b]
-
David Evans.
LCLint User's Guide, Version 2.1, April 1996.
Available at the following URL
`http://www.sds.lcs.mit.edu/spd/larch/lclint/guide/'.
- [Goguen84]
-
Joseph A. Goguen.
Parameterized Programming.
IEEE Transactions on Software Engineering,
10(5):528-543 (Sept. 1984).
- [Guaspari-Marceau-Polak90]
-
David Guaspari, Carla Marceau, and Wolfgang Polak.
Formal Verification of Ada Programs.
IEEE Transactions on Software Engineering,
16(9):1058-1075 (Sept. 1990).
- [Guttag-Horning-Wing85b]
-
John V. Guttag and James J. Horning and Jeannette M. Wing.
The Larch Family of Specification Languages.
IEEE Software, 2(5):24-36 (Sept. 1985).
- [Guttag-Horning78]
-
J. Guttag and J. J. Horning.
The Algebraic Specification of Abstract Data Types.
Acta Informatica,
10(1):27-52 (1978).
- [Guttag-Horning91b]
-
J. V. Guttag and J. J. Horning.
A Tutorial on Larch and LCL, a Larch/C Interface Language.
In S. Prehn and W. J. Toetenel (eds.),
VDM '91 Formal Software Development Methods 4th
International Symposium of VDM Europe
Noordwijkerhout, The Netherlands, Volume 2: Tutorials.
Lecture Notes in Computer Science, vol. 552,
(Springer-Verlag, NY, 1991), pages 1-78.
- [Guttag-Horning93]
-
John V. Guttag and James J. Horning with S.J. Garland,
K.D. Jones, A. Modet and J.M. Wing.
Larch: Languages and Tools for Formal Specification
(Springer-Verlag, NY, 1993).
(The ISBN numbers are 0-387-94006-5 and 3-540-94006-5.)
The traits in Appendix A (the "Handbook")
are found on-line at the following URL
`http://www.research.digital.com/SRC/larch/'.
- [Hall90]
-
Anthony Hall.
Seven Myths of Formal Methods.
IEEE Software, 7(5):11-19 (Sept. 1990).
- [Hayes93]
-
I. Hayes (ed.),
Specification Case Studies, second edition
(Prentice-Hall, Englewood Cliffs, N.J., 1990).
- [Hesselink92]
-
Wim H. Hesselink.
Programs, Recursion, and Unbounded Choice
(Cambridge University Press, Cambridge, UK, 1992).
- [Hoare69]
-
C. A. R. Hoare.
An Axiomatic Basis for Computer Programming.
Comm. ACM, 12(10):576-583 (Oct. 1969).
- [Hoare72a]
-
C. A. R. Hoare.
Proof of correctness of data representations.
Acta Informatica, 1(4):271-281 (1972).
- [Jones86b]
-
Cliff B. Jones,
Systematic software development using VDM,
(Prentice-Hall, Englewood Cliffs, N.J., 1986).
- [Jones95e]
-
C.B. Jones,
Partial functions and logics: A warning.
Information Processing Letters, 54(2):65-67, 1995.
- [Jones91]
-
Kevin D. Jones,
LM3: A Larch Interface Language for Modula-3: A
Definition and Introduction: Version 1.0.
Technical Report 72, Digital Equipment Corp, Systems Research Center,
130 Lytton Avenue Palo Alto, CA 94301, June, 1991.
Order from src-report@src.dec.com or from the URL
`http://www.research.digital.com/SRC/publications/src-rr.html'.
- [Jonkers91]
-
H. B. M. Jonkers.
Upgrading the pre- and postcondition technique.
In S. Prehn and W. J. Toetenel (eds.),
VDM '91 Formal Software Development Methods 4th
International Symposium of VDM Europe
Noordwijkerhout, The Netherlands, Volume 1:
Conference Contributions,
volume 551 of Lecture Notes in Computer Science,
pages 428-456.
Springer-Verlag, NY, 1991.
- [Kiczales-Lamping92]
-
Gregor Kiczales and John Lamping.
Issues in the Design and Documentation of Class Libraries.
In Andreas Paepcke (ed.), OOPSLA '92 Proceedings
(ACM SIGPLAN Notices, 27(10):435-451, Oct., 1992).
- [Lamport89]
-
Leslie Lamport.
A Simple Approach to Specifying Concurrent Systems.
CACM, 32(1):32-45 (Jan. 1989).
- [Leavens-Baker99]
-
Gary T. Leavens and Albert L. Baker.
Enhancing the Pre- and Postcondition Technique for
More Expressive Specifications.
Department of Computer Science, Iowa State University,
TR #97-19a, September 1997, revised February 1999
which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR97-19/TR.ps.gz'.
- [Leavens-Cheon92b]
-
Gary T. Leavens and Yoonsik Cheon.
Preliminary Design of Larch/C++.
In [Martin-Wing93], pages 159-184.
- [Leavens-Weihl90]
-
Gary T. Leavens and William E. Weihl.
Reasoning about Object-oriented Programs that use Subtypes
(extended abstract).
In N. Meyrowitz (ed.), OOPSLA ECOOP '90 Proceedings
(ACM SIGPLAN Notices, 25(10):212-223, Oct., 1990).
- [Leavens-Weihl95]
-
Gary T. Leavens and William E. Weihl.
Specification and Verification of Object-Oriented
Programs Using Supertype Abstraction.
Acta Informatica, 32(8):705-778 (Nov. 1995).
- [Leavens90]
-
Gary T. Leavens.
Modular Verification of Object-Oriented Programs with Subtypes.
Department of Computer Science, Iowa State University (Ames, Iowa, 50011),
TR 90-09, July 1990.
Available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR90-09/TR.ps.Z'.
- [Leavens91]
-
Gary T. Leavens.
Modular Specification and Verification of Object-Oriented Programs.
IEEE Software, 8(4):72-80 (July 1991).
- [Leavens96]
-
Gary T. Leavens.
An Overview of Larch/C++: Behavioral Specifications for C++ Modules.
In Haim Kilov and William Harvey (editors),
Specification of Behavioral Semantics in Object-Oriented Information
Modeling (Kluwer Academic Publishers, 1996), Chapter 8, pages 121-142.
An extended version is
Department of Computer Science, Iowa State University,
TR #96-01c, July 1996,
which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR96-01/TR.ps.Z'.
- [Leavens98]
-
Gary T. Leavens.
Larch Frequently Asked Questions.
Department of Computer Science, Iowa State University,
August 1998.
Available from the URL
`http://www.cs.iastate.edu/~leavens/larch-faq.html'.
- [Ledgard80]
-
Henry. F. Ledgard.
A Human Engineered Variant of BNF.
ACM SIGPLAN Notices, 15(10):57-62 (October 1980).
- [Leino95]
-
K. Rustan M. Leino.
Towards Reliable Modular Programs.
PhD thesis, California Institute of Technology, January 1995.
Available from the URL
`ftp://ftp.cs.caltech.edu/tr/cs-tr-95-03.ps.Z'.
- [Leino95b]
-
K. Rustan M. Leino.
A myth in the modular specification of programs.
KRML 63, November 1995.
Obtained from the author (rustan@pa.dec.com).
- [Lerner91]
-
Richard Allen Lerner.
Specifying Objects of Concurrent Systems.
School of Computer Science, Carnegie Mellon University,
CMU-CS-91-131, May 1991.
Available from the URL
`ftp://ftp.cs.cmu.edu/afs/cs.cmu.edu/project/larch/ftp/thesis.ps.Z'.
- [Liskov-Guttag86]
-
Barbara Liskov and John Guttag.
Abstraction and Specification in Program Development
(MIT Press, Cambridge, Mass., 1986).
- [Liskov-Wing93]
-
Barbara Liskov and Jeannette M. Wing.
A new definition of the subtype relation.
In Oscar M. Nierstrasz, editor, ECOOP '93 -- Object-Oriented
Programming, 7th European Conference, Kaiserslautern, Germany,
volume 707 of Lecture Notes in Computer Science,
pages 118-141. Springer-Verlag, New York, N.Y., July 1993.
- [Liskov-Wing93b]
-
Barbara Liskov and Jeannette M. Wing.
Specifications and their use in defining subtypes.
In Andreas Paepcke, editor, OOPSLA '93 Proceedings,
volume 28, number 10 of ACM SIGPLAN Notices, pages 16-28.
ACM Press, October 1993.
- [Liskov-Wing94]
-
Barbara Liskov and Jeannette M. Wing.
A Behavioral Notion of Subtyping.
ACM TOPLAS, 16(6):1811-1841 (Nov. 1994).
- [Martin-Wing93]
-
U. Martin and J. Wing.
Proceedings of the First International Workshop on Larch,
July 1992.
Workshops in Computing series (Springer-Verlag, New York, 1993).
(The ISBN is 0-387-19804-0.)
- [Meyer88]
-
Bertrand Meyer.
Object-oriented Software Construction
(Prentice-Hall, 1988).
- [Meyer92]
-
Bertrand Meyer.
Applying "Design by Contract".
Computer, 25(10):40-51 (Oct. 1992).
- [Meyer92b]
-
Bertrand Meyer.
Eiffel: The Language
(Prentice-Hall, 1992).
- [Morgan94]
-
Carroll Morgan.
Programming from Specifications, second edition
(Prentice-Hall, 1994).
- [Morris87]
-
Joseph~M. Morris.
A theoretical basis for stepwise refinement and the programming
calculus.
Science of Computer Programming, 9(3):287-306, December 1987.
- [Nelson89]
-
Greg Nelson.
A Generalization of Dijkstra's Calculus.
ACM Transactions on Programming Languages and Systems,
11(4):517-561 (Oct. 1989).
- [Parnas72]
-
D. L. Parnas.
On the Criteria to be Used in Decomposing Systems into Modules.
Comm. ACM, 15(12) (Dec., 1972).
- [Poetzsch-Heffter97]
-
Arnd Poetzsch-Heffter.
Specification and Verification of Object-Oriented Programs.
Habilitationsschrift, Technische Universitaet Muenchen, 1997.
Available from the URL
`http://wwweickel.informatik.tu-muenchen.de/persons/poetzsch/habil.ps.gz'.
- [Schmidt86]
-
David A. Schmidt.
Denotational Semantics: A Methodology for Language Development
(Allyn and Bacon, Inc., Boston, Mass., 1986).
- [Spivey92]
-
J. Michael Spivey.
The Z Notation: A Reference Manual, second edition,
(Prentice-Hall, Englewood Cliffs, N.J., 1992).
- [Steyaert-etal96]
-
Patrick Steyaert, Carine Lucas, Kim Mens, and Theo D'Hondt.
Issues in the Design and Documentation of Class Libraries.
In OOPSLA '96 Proceedings
(ACM SIGPLAN Notices, 31(10):268-285, Oct., 1996).
- [Stroustrup91]
-
B. Stroustrup.
The C++ Programming Language: Second Edition
(Addison-Wesley Publishing Co., Reading, Mass., 1991).
- [Stroustrup95]
-
B. Stroustrup.
ANSI/ISO Resolutions.
File date February 13, 1995.
Obtained by anonymous ftp from the URL
`ftp://ftp.std.com/AW/stroustrup2e/new_iso.ps'.
- [Tan94]
-
Yang Meng Tan.
Formal Specification Techniques for Promoting Software Modularity,
Enhancing Documentation, and Testing Specifications.
MIT Lab. for Comp. Sci., TR 619, June 1994.
Also published as Formal Specification Techniques for Engineering
Modular C Programs.
International Series in Software Engineering
(Kluwer Academic Publishers, Boston, 1995).
- [Watt91]
-
David A. Watt.
Programming Language Syntax and Semantics.
Prentice Hall, International Series in Computer Science,
New York, 1991.
- [Wills92b]
-
Alan Wills.
Specification in Fresco.
In Susan Stepney and Rosalind Barden and David Cooper (eds.),
Object Orientation in Z, chapter 11, pages 127-135.
Springer-Verlag, Workshops in Computing Series, Cambridge CB2 1LQ, UK,
1992.
- [Wing83]
-
Jeannette Marie Wing.
A Two-Tiered Approach to Specifying Programs
Technical Report TR-299, Mass. Institute of Technology,
Laboratory for Computer Science, 1983.
- [Wing87]
-
Jeannette M. Wing.
Writing Larch Interface Language Specifications.
ACM Transactions on Programming Languages and Systems,
9(1):1-24 (Jan. 1987).
- [Wing90a]
-
Jeannette M. Wing.
A Specifier's Introduction to Formal Methods.
Computer, 23(9):8-24 (Sept. 1990).
- [Wing90b]
-
Jeannette M. Wing.
Using Larch to Specify Avalon/C++ Objects.
IEEE Transactions on Software Engineering,
16(9):1076-1088 (Sept. 1990).
Go to the first, previous, next, last section, table of contents.