The Larch/C++ Project

Contents:

About Larch/C++
Other Larch Resources
- General including the Larch FAQ
- Larch Shared Language (LSL)
Staff
Acknowledgements

There is also a page describing local Iowa State Details related to Larch/C++.

The following documents are listed in the order in which someone learning Larch/C++ might benefit from reading them. The first is a very brief overview of Larch/C++. The documents below are either HTML or text files. Postscript and dvi versions of these documents are also available from the Larch/C++ ftp directory; however, note that the reference manual is over 300 pages long. The Larch/C++ release also contains most of these documents in HTML format, if you wish to browse them locally.

Gary T. Leavens. Larch/C++ An Interface Specification Language for C++, Iowa State University, August 1997. This is also available in [postscript] and [dvi] formats.
Gary T. Leavens. An Overview of Larch/C++: Behavioral Specifications for C++ Modules. Adapted from Haim Kilov and William Harvey (editors), Specification of Behavioral Semantics in Object-Oriented Information Modeling (Kluwer Academic Publishers, 1996), Chapter 8, pages 121-142. This revised version is also available in [postscript] and [dvi] formats.
Samples directory of specifications written in Larch/C++
Exercises directory for learning about Larch/C++ (very incomplete).
Gary T. Leavens. Larch/C++ Reference Manual, Iowa State University, Version 5.41, April 1999. This is also available in [postscript] and [dvi] formats. Beware, the postscript and dvi files are big, since the manual is over 300 pages long.
LSL traits that are built-in to Larch/C++

Other papers about Larch/C++

The following papers give more details on Larch/C++. All but the first are somewhat obsolete. They are listed in reverse cronological order, so the ones at the top of the list are less out of date than those at the bottom. Most are only available in postscript format.

Gary T. Leavens and Albert L. Baker. Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. In Jeannette Wing and James Woodcock, editors. FM'99: 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.
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.
Matthew W. Markland. Design and Implementation of the Larch/C++ Type System. Department of Computer Science, Iowa State University, TR #98-05, June 1998.
David M. Egle. Evaluating Larch/C++ as a Specification Language: A Case Study Using the Microsoft Foundation Class Library. Department of Computer Science, Iowa State University, TR #95-17, July 1995.
John Penix's page on the time warp simulation kernel.
Yoonsik Cheon and Gary T. Leavens. A Quick Overview of Larch/C++. Journal of Object-Oriented Programming, 7(6):39-49, October 1994.
Gary T. Leavens and Yoonsik Cheon. Preliminary Design of Larch/C++. In U. Martin and J. Wing, editors, Proc. First International Workshop on Larch, Dedham 1992, pages 159-184. Workshops in Computing Series. Springer-Verlag, 1993.

See also Gary T. Leavens's research page for less directly related publications.

Getting the Larch/C++ Release

The Larch/C++ release is currently in beta-test. It can be obtained from the ftp directory listed below.

To get a version that runs under Windows 95, get the latest file name LCPPWin.*.zip, where * is a number like 5.14.

To get a source version, which you can compile and install under Unix (and possibly other operating systems) get the latest file name LCPP.*.tar.gz, where * is a number like 5.14.

You will also need the LSL checker.

Larch/C++ ftp directory, which contains among other things:
- README file for the release
- COPYRIGHT file for the release
- NEWS file for the release
Larch ftp directory, contains the LSL checker releases.
Boehm-Demers-Weiser conservative garbage collector ftp directory.
The lcpp2html conversion utility is part of the Larch/C++ release, but can also be obtained separately.
The Larch Prover (LP) is optional, but useful for debugging LSL traits.
The Larch Development Environment (LDE) from Betty Cheng's group in the Computer Science Department at Michigan State University, is a graphical user interface which helps develop LSL and Larch/C++ specifications.

You can also browse our to do list to read about our plans for the Larch/C++ tools.

E-Mail for help with Larch/C++

If you have a comment about Larch/C++, or a question that isn't answered in the documentation, send e-mail to us at lc++@cs-DOT-iastate-DOT-edu (replace -DOT- by .).

2. Other Larch Resources

General

See the comp.specification.larch usenet newsgroup.
Larch FAQ (frequently asked questions with answers).
MIT Larch page
Jim Horning's Larch page.

You should also read at least chapters 1-4 of the book: J.V. Guttag and J.J. Horning, Larch: Languages and Tools for Formal Specification, (Springer-Verlag, 1993).

Larch Shared Language (LSL)

Guttag and Horning's Handbook of LSL traits.
Gary Leavens's handbooks page (a guide to other LSL Handbooks, and hypertext for the traits).

3. Staff

Gary T. Leavens is guiding the work on Larch/C++. Also working on various aspects are Robert Lavey, Matt Markland, Clyde Ruby, Hua Zhong.

In the past, major contributions were made by graduate student Yoonsik Cheon. A recent Ph.D. student, Krishna Kishore Dhara, has been working on theoretical aspects related to Larch/C++. Also in the past, Tim Wahls, Dave Egle, Rhadika Allada, and Matt Shores have helped on various aspects of Larch/C++.

4. Acknowledgements

The development of Larch/C++ was partially funded by a research initiation grant from the (US) National Science Foundation in 1991, and is currently funded by NSF grants CCR-9503168 and CCR-9803843.

See the Larch/C++ Reference Manual for full acknowledgements.

Gary T. Leavens

Last update $Date: 2007/08/10 23:10:51 $

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.