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 exec ...

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 Execution (computing), execute. It is one component of software, which also includes software documentation, documentation and other intangibl ...

s and the formulation of proofs about program behavior. The Larch family was developed primarily in the

United States The United States of America (USA), also known as the United States (U.S.) or America, is a country primarily located in North America. It is a federal republic of 50 U.S. state, states and a federal capital district, Washington, D.C. The 48 ...

in the 1980s and 1990s, involving researchers at

Xerox PARC Future Concepts division (formerly Palo Alto Research Center, PARC and Xerox PARC) is a research and development company in Palo Alto, California. It was founded in 1969 by Jacob E. "Jack" Goldman, chief scientist of Xerox Corporation, as a div ...

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 university, private research university in Cambridge, Massachusetts, United States. Established in 1861, MIT has played a significant role in the development of many areas of moder ...

(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 ...

abstract data type In computer science, an abstract data type (ADT) is a mathematical model for data types, defined by its behavior (semantics) from the point of view of a '' user'' of the data, specifically in terms of possible values, possible operations on data ...

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+. It has been influential in research circles (influencing the designs of languages such as Java, C#, Python and Nim), but it ha ...

Smalltalk Smalltalk is a purely object oriented programming language (OOP) that was originally created in the 1970s for educational use, specifically for constructionist learning, but later found use in business. It was created at Xerox PARC by Learni ...

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

References

External links

*
CASL, The Common Algebraic Specification Language
{{Prog-lang-stub Formal specification languages

See also

References

External links