This work was supported in part by the United States National Science Foundation under Grants CCR-9108654, CCR-9503168, and CCR-9803843.
I gratefully acknowledge the large contributions made by Yoonsik Cheon. Yoonsik has been there from the beginning, helped design Larch/C++, helped implement the initial versions of the Larch/C++ parser, helped design and manage the release, and helped write several technical papers and the initial versions of this manual. His advice on technical matters is always valuable, and in large part Larch/C++ would not exist without his aid.
I am also very grateful to Clyde Ruby, who during 1998 and early 1999 spent large amounts of time wrestling with the difficult C++ grammar, and getting our tools into better shape. He also updated the grammar in this reference manual, and has helped with various new parts of the syntax, notably the calls-clause, the accesses-clause, and the represents-clause. We've also consulted about the design, syntax, and semantics of behavior programs. Thanks Clyde!
Special thanks to Jeannette Wing for suggesting this research project, and for providing hints for Larch/C++ in her paper on Avalon/C++ [Wing90b].
Thanks to Jim Horning, John Guttag, and Yang Meng Tan for their design of
LCL (a Larch/C).
Thanks to Yoonsik Cheon,
Krishna Kishore Dhara, Matt Markland, Clyde Ruby, Hua Zhong,
Albert Baker, and Tim Wahls for many discussions on
technical matters related to Larch/C++.
Al Baker's insistence that specifiers should be able to do a lot
without writing complex traits is, I hope finally realized in
of Larch/C++; thanks!
Thanks also to Al for help with the syntax and semantics of redundancy.
Thanks to participants in the Object-Oriented Formal Methods seminar
during Fall 1993,
the Formal Methods seminar of Summer 1992,
the seminar on the Development of Larch-style
Interface Specification Languages in Fall 1994,
and the seminar on Specification and Verification with Larch/C++
in Fall 1995.
Thanks to Mark Vandevoorde, Dave Detlefs, and Yang Meng Tan
for a series of personal communications about the semantics of trashed.
Thanks to Dave Evans and especially to Patrice Chalin
for a series of personal communications about the semantics of trashed
and the modifies-clause.
Patrice finally convinced me that his semantics was better; thanks!
Thanks to Rustan Leino for his work on the semantics of dependencies,
and several discussions about it and its implications for Larch/C++.
Thanks to Peter Mueller for a correction to the semantics of invariants
and their explanation,
which was also applied to the semantics of constraints.
Thanks to Dave Musser and participants at the Dagsthul workshop on
generic programming for discussions about generic programming and templates.
Thanks to Radhika Allada and Bob Lavey for help with some of the tools. Thanks to Dave Egle for being an excellent user and evaluator of Larch/C++. Thanks to Kurt Bischoff for developing his attribute grammar evaluator, Ox, and for his support of that software. Thanks to Kelvin Nilsen, who supervised the development of Ox, and who helped with using it. Thanks to Hans Boehm for his conservative garbage collector software, and his help in using it correctly. Thanks to Matt Markland for getting namespace support and checking of LSL traits into the Larch/C++ checker. Thanks to Clyde Ruby for much work on caching of traits in the implementation, and for helping with the calls-clause.
Thanks to Piero Colagrosso, K. Kishore Dhara, Dave Egle, Sudipto Ghosh, Marybeth Gurski, John Guttag, Mike Haverdink, Jim Horning, Steve Jenkins, Kevin Jones, Bob Lavey, Rustin Leino, Jacek Leszczylowski, Matt Markland, Tong Mei, John Penix, Antonios Protopsaltou, Arnd Poetzsch-Heffter, John Rood, John Rose, Pierre-Yves Schobbens, Ulf Schuenemann, Tapas Shomee, David Sims, Gowri Sivaprasad, Yang Meng Tan, Tim Wahls, Jeannette Wing, and others we may have forgotten for comments about Larch/C++ and drafts of this manual. Thanks to Patrice Chalin for comments about LCL [Chalin95] [Chalin-etal96] and for email discussions, which lead to some significant semantic improvements in Larch/C++. Thanks to Hua Zhong for improvements to the traits used in htis manual that have emerged from her proofs of their implications.
Thanks to Matt Markland, David Cok, Dave Egle, Albert Esterline, Steve Freeman, Ward Harold, Bob Lavey, Thomas Lindner, Tim Wahls, and others for bug reports and help with portability. Thanks to Madhu Rajmani for finding out about the texi2html program.
Go to the first, previous, next, last section, table of contents.