Server: Netscape-Commerce/1.12 Date: Tuesday, 26-Nov-96 00:06:29 GMT Last-modified: Thursday, 15-Jun-95 00:07:12 GMT Content-length: 2745 Content-type: text/html
![]() |
![]() |
![]() |
John Guttag, Group Head | Stephen Garland, Principal Research Scientist | Mark T. Vandevoorde, Research Scientist |
The Larch project is designed to help produce high-quality computer systems through the practical application of rigorous methods of software and hardware design, development, and maintenance.
Collaborating with systems designers, we study methods for "decomposing" designs into modules with well-defined interfaces and specifying the behavior of these interfaces. This approach makes it easier to reason about designs, since one can rely on specifications instead of examining implementations.
An extensive set of support tools is an important part of Larch. Some of the tools are lightweight -- that is, they are quick and easy to use. LCLint, for example, supports programming with data abstractions in ANSI C by detecting obvious conflicts between code and interface specifications.
Other tools are more heavyweight and so require more time and expertise. The theorem-proving system called LP, for instance, supports reasoning (in first-order logic) about the properties of abstractions and designs. Proofs, like designs, must be created, debugged, and maintained. Since LP is used early in the design process to find design flaws, it treats proving as an activity similar to programming. All Larch tools support incremental development in that they work with partial specifications, but repay larger specification investments with larger dividends in analysis.
The Larch project is becoming increasingly involved with the design of parallel and distributed systems. Our aim is to develop a useful set of abstractions and implementation techniques for producing concurrent interactive symbolic applications.