The Larch family of formal
specification language
A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the execu ...
s are intended for the precise specification of computing systems. They allow the clean specification of
computer program
A computer program is a sequence or set of instructions in a programming language for a computer to execute. Computer programs are one component of software, which also includes documentation and other intangible components.
A computer program ...
s and the formulation of
proofs about program behavior.
The Larch family was developed primarily in the
United States
The United States of America (U.S.A. or USA), commonly known as the United States (U.S. or US) or America, is a country primarily located in North America. It consists of 50 states, a federal district, five major unincorporated territori ...
in the 1980s and 1990s, involving researchers at
Xerox PARC
PARC (Palo Alto Research Center; formerly Xerox PARC) is a research and development company in Palo Alto, California. Founded in 1969 by Jacob E. "Jack" Goldman, chief scientist of Xerox Corporation, the company was originally a division of Xero ...
,
DEC Systems Research Center
The Systems Research Center (SRC) was a research laboratory created by Digital Equipment Corporation (DEC) in 1984, in Palo Alto, California.
DEC SRC was founded by a group of computer scientists, led by Robert Taylor, who left the Computer ...
(DEC/SRC),
Massachusetts Institute of Technology
The Massachusetts Institute of Technology (MIT) is a private land-grant research university in Cambridge, Massachusetts. Established in 1861, MIT has played a key role in the development of modern technology and science, and is one of the ...
(MIT), and other places. Unlike the
Z notation
The Z notation 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
In 1974, Jean-Raymond Abria ...
, the Larch family has one language for
algebraic specification Algebraic specification is a software engineering technique for formally specifying system behavior. It was a very active subject of computer science research around 1980.
Overview
Algebraic specification seeks to systematically develop more effic ...
of
abstract data type
In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a ''user'', of the data, specifically in terms of possible values, pos ...
s (the ''Larch Shared Language'' (LSL)), and a separate ''interface language'' tailored to each language in which programs are to be written, such as
C,
Modula-3
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 (influencing the designs of languages such as Java, C#, and Python) it has not ...
,
Smalltalk, etc. The Larch project also developed tools to support the use of formal specifications, including the
Larch Prover (LP).
See also
*
Formal methods
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...
References
External links
*
CASL, The Common Algebraic Specification Language
{{Prog-lang-stub
Formal specification languages