The papers in this volume were presented at the First International Workshop on Larch, held at MIT Endicott House near Boston on 13-15 July 1992. Larch is a family of formal specification languages and tools, and this workshop was a forum for those who have designed the Larch languages, built tool support for them, particularly the Larch Prover, and used them to specify and reason about software and hardware systems. The Larch Project started in 1980, led by John Guttag at MIT and James Horning, then at Xerox/Palo Alto Research Center and now at Digital Equipment Corporation/Systems Research Center (DEC/SRC). Major applications have included VLSI circuit synthesis, medical device communications, compiler development and concurrent systems based on Lamport's TLA, as well as several applications to classical theorem proving and algebraic specification. Larch supports a two-tiered approach to specifying software and hardware modules. One tier of a specification is wrillen in the Larch Shared Language (LSL). An LSL specification describes mathematical abstractions such as sets, relations, and algebras; its semantics is defined in terms of first-order theories. The second tier is written in a Larch interface language, one designed for a specific programming language. An interface specification describes the effects of individual modules, e.g. state changes, resource allocation, and exceptions; its semantics is defined in terms of first-order predicates over two states, where state is defined in terms of the programming language's notion of state. Thus, LSL is programming language independent; a Larch interface language is programming language dependent.

Klappentext

The Larch family of formal specification languages and tools was originally developed in the USA. Its user community has now spread to Europe and several industrial firms are interested in using it in their system development programs. It differs from the other "higher profile" languages such as Z and VDM in three respects: firstly, it was designed to specify programs rather than mathematical models and therefore addresses the complexities of real programs; secondly, it has been specifically developed as a practical tool for use in several major application domains; finally, it has a state-of-the-art semantic analysis tool in the form of the Larch Prover. This volume contains the papers presented at the First International Workshop on Larch, held in Dedham, USA, 13-15 July 1992. The workshop brought together for the first time those who have designed the Larch languages, built tool support for them, and used them to specify and reason about soft- and hardware systems. It encouraged discussion about how the Larch languages and Prover are being used, and assessed plans for developing them. The aim of the workshop was to raise the profile of Larch, and to provide impetus for continued research into its tools and languages. Among the topics covered in this volume are: the mechanical verification of concurrent systems with TLA; the DECspec project; the preliminary design of Larch/C++; generating proof obligations for circuits; lock-level verification; checking software design using formal specifications; optimizing programs with specifications; a report on the formal basis of generics. First International Workshop on Larch provides a comprehensive overview of the international use and development of Larch. It will be invaluable to researchers and practitioners who are already involved with, or who wish to know more about, this important specification language.

Inhalt
Is Engineering Software Amenable to Formal Specification?.- How to Prove Observational Theorems with LP.- Using SOS Definitions in Term Rewriting Proofs.- An exercise in LP: The Proof of a Non Restoring Division circuit.- Integrating ASSPEGIQUE and LP.- Mechanical Verification of Concurrent Systems with TLA.- The DECspec Project: Tools for Larch/C.- Formal Verification of Ada Programs.- A Semantics for a Larch/Modula-3 Interface Language.- Preliminary Design of Larch/C++.- Generating Proof Obligations for Circuits.- Using Transformations and Verification in Circuit Design.- Using LP to Study the Language PL 0 + .- Semantic Analysis of Larch Interface Specifications.- Optimizing Programs with Partial Specifications.- A new Front-End for the Larch Prover.- Thoughts on a Larch/ML and a New Application for LP.