Workshops in Computing

First International Workshop on Larch

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

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

Buy this book

eBook $74.99
price for USA (gross)
  • ISBN 978-1-4471-3558-6
  • Digitally watermarked, DRM-free
  • Included format: PDF
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Softcover $99.00
price for USA
  • ISBN 978-3-540-19804-8
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
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.

Table of contents (17 chapters)

  • Is Engineering Software Amenable to Formal Specification?

    Baugh, John W.

    Pages 1-17

  • How to Prove Observational Theorems with LP

    Bidoit, Michel (et al.)

    Pages 18-35

  • Using SOS Definitions in Term Rewriting Proofs

    Buth, Karl-Heinz

    Pages 36-54

  • An exercise in LP: The Proof of a Non Restoring Division circuit

    Chetali, Boutheina (et al.)

    Pages 55-68

  • Integrating ASSPEGIQUE and LP

    Choppy, Christine (et al.)

    Pages 69-85

Buy this book

eBook $74.99
price for USA (gross)
  • ISBN 978-1-4471-3558-6
  • Digitally watermarked, DRM-free
  • Included format: PDF
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Softcover $99.00
price for USA
  • ISBN 978-3-540-19804-8
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
Loading...

Recommended for you

Loading...

Bibliographic Information

Bibliographic Information
Book Title
First International Workshop on Larch
Book Subtitle
Proceedings of the First International Workshop on Larch, Dedham, Massachusetts, USA, 13–15 July 1992
Editors
  • Ursula Martin
  • Jeannette M. Wing
Series Title
Workshops in Computing
Copyright
1993
Publisher
Springer-Verlag London
Copyright Holder
Springer-Verlag London
eBook ISBN
978-1-4471-3558-6
DOI
10.1007/978-1-4471-3558-6
Softcover ISBN
978-3-540-19804-8
Series ISSN
1431-1682
Edition Number
1
Number of Pages
VIII, 315
Number of Illustrations and Tables
4 b/w illustrations
Additional Information
Jointly published with the British Computer Society
Topics