Logo - springer
Slogan - springer

Computer Science - Software Engineering | First International Workshop on Larch - Proceedings of the First International Workshop on Larch,

First International Workshop on Larch

Proceedings of the First International Workshop on Larch, Dedham, Massachusetts, USA, 13–15 July 1992

Martin, Ursula, Wing, Jeannette M. (Eds.)

Jointly published with the British Computer Society

1st Edition., VIII, 315 p.

Available Formats:

Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.

You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.

After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.


(net) price for USA

ISBN 978-1-4471-3558-6

digitally watermarked, no DRM

Included Format: PDF

download immediately after purchase

learn more about Springer eBooks

add to marked items


Softcover (also known as softback) version.

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-3-540-19804-8

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days

add to marked items

  • About this book

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.

Content Level » Research

Keywords » Ada - C++ programming language - ML - Mathematica - Modula-3 - design - development - formal specification - language - programming - programming language - semantics - software - system development - verification

Related subjects » Software Engineering - Theoretical Computer Science

Table of contents 

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.

Popular Content within this publication 



Read this Book on Springerlink

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Software Engineering.