The Larch family of formal specification language

Specification language

A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...

s are intended for the precise specification of computing systems. They allow the clean specification of computer program

Computer program

A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...

s and the formulation of proofs about program behavior.

The Larch family was developed primarily in the United States

United States

The United States of America is a federal constitutional republic comprising fifty states and a federal district...

 in the 1980s and 1990s, involving researchers at Xerox PARC

Xerox PARC

PARC , formerly Xerox PARC, is a research and co-development company in Palo Alto, California, with a distinguished reputation for its contributions to information technology and hardware systems....

, DEC/SRC

DEC Systems Research Center

The Systems Research Center was a research laboratory created by Digital Equipment Corporation in 1984, in Palo Alto, California....

, MIT, and other places. Unlike the Z notation

Z notation

The Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...

, the Larch family has one language for algebraic specification

Algebraic specification

Algebraic specification, is a software engineering technique for formally specifying system behavior. Algebraic specification seeks to systematically develop more efficient programs by:...

 of abstract data types (LSL, the Larch Shared Language), and a separate interface language tailored to each language in which programs are to be written (Modula-3

Modula-3

In computer science, Modula-3 is a programming language conceived as a successor to an upgraded version of Modula-2 known as Modula-2+. While it has been influential in research circles it has not been adopted widely in industry...

, C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

, Smalltalk

Smalltalk

Smalltalk is an object-oriented, dynamically typed, reflective programming language. Smalltalk was created as the language to underpin the "new world" of computing exemplified by "human–computer symbiosis." It was designed and created in part for educational use, more so for constructionist...

, etc.). The Larch project also developed tools to support the use of formal specifications, including LP, the Larch Prover

Larch Prover

Larch Prover, or LP for short, is an interactive theorem proving system for multisorted first-order logic. It is currently used at MIT and elsewhere to reason about designs for circuits, concurrent algorithms, hardware, and software...

.

External links

• MIT Larch home page.
• Larch: Languages and Tools for Formal Specification (.PDF), Springer-Verlag
  Springer Science+Business Media
  - Selected publications :* Encyclopaedia of Mathematics* Ergebnisse der Mathematik und ihrer Grenzgebiete * Graduate Texts in Mathematics * Grothendieck's Séminaire de géométrie algébrique...
  
  (1993). ISBN 0-387-94006-5
• CASL, The Common Algebraic Specification Language.