An overview of Larch

Stephen J. Garland, John V. Guttag, and James J. Horning

Functional Programming, Concurrency, Simulation, and Automated Reasoning

Lecture Notes in Computer Science 693, Peter E. Lauer (editor), Springer-Verlag, 1993, pages 329-348

Abstract

We begin by describing the Larch approach to specification and illustrating it with a few small examples. We then discuss LP, the Larch proof assistant, a tool that supports all the Larch languages. Our intent is to give you only a taste of these things. For a comprehensive look at Larch see John V. Guttag and James J. Horning (editors), with Stephen J. Garland, Kevin D. Jones, Andres Modet, and Jeannette M. Wing, Larch: Languages and Tools for Formal Specification, Springer-Verlag Texts and Monographs in Computer Science, 1993.