## Larch: Languages and Tools for Formal SpecificationThis text addresses an important topic: the use of a formal specification language and supporting tools. Formal methods are becoming increasingly important to the practicing programmer; "Springer-Verlag" has a tradition of publishing books in this area. The book's subject, the Larch specification work at MIT and DEC, is respected amongst academic computer scientists. As plans begin for Larch tools to be distributed to the community, this book can serve as an invaluable reference. The authors of this text, James Horning and John Guttag, want their book to reach people interested in implementing formal methods into practical use. This readable text makes extensive use of examples, and serves as both a reference manual and as a tutorial. "Chapter" "1" discusses the use of formal specifications in program development, providing a context for the technical material that follows. "Chapter 2" contains a very short introduction to the notation of mathematical logic. The chapter is aimed at those with no background in logic, and provides all the logic background needed to understand the remainder of the book. The remaining six chapters of the book contains an in-depth look at Larch, and the authors' approach to the formal specification of program components. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Specifications in Program Development | 1 |

A Little Bit of Logic | 8 |

An Introduction to Larch | 14 |

Copyright | |

7 other sections not shown

### Other editions - View all

Larch: Languages and Tools for Formal Specification John V. Guttag,James J. Horning Limited preview - 2012 |

Larch: Languages and Tools for Formal Specification John V. Guttag,James J. Horning No preview available - 2011 |

Larch: Languages and Tools for Formal Specification John V. Guttag,James J. Horning No preview available - 2012 |

### Common terms and phrases

abstract type axioms Bool asserts Chapter char checking clients Computer Science conjecture contains count data structures data type dbase DEC/SRC declare deduction rule define employee EmployeeSet empset empty ensures clause ensures result equations ercIter eref erefNIL ereftab example files first-order logic floating point formal specification Guttag illus implementation implies converts induction insert InsertGenerated interface specifications isEmpty John Guttag Larch interface language Larch Prover Larch Shared Language LinearContainer logical lookup LSL Checker LSL specifications maxTabSize methods modifies Modula-3 modules numAdded object operators partitioned post-state postcondition pre-state predicate procedure programming language proof obligations prove provides queue range sort requires clause rewrite rules SELF.manager SELF.set semantic sort ssNum strict partial orders struct subgoal succ succ(x synonym tail theorem theory TotalOrder TotOrd trait assumes trait includes trait introduces true tuple typedef values variable void written