The Larch family of formal
specification languages are intended for the precise specification of computing systems. They allow the clean specification of
computer programs and the formulation of
proofs about program behavior.
The Larch family was developed primarily in the
United States in the 1980s and 1990s, involving researchers at
Xerox PARC,
DEC Systems Research Center (DEC/SRC),
Massachusetts Institute of Technology (MIT), and other places. Unlike the
Z notation, the Larch family has one language for
algebraic specification of
abstract data types (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,
Smalltalk
Smalltalk is an object-oriented, dynamically typed reflective programming language. It was designed and created in part for educational use, specifically for constructionist learning, at the Learning Research Group (LRG) of Xerox PARC by Alan Ka ...
, etc. The Larch project also developed tools to support the use of formal specifications, including the
Larch Prover
The Larch Prover, or LP for short, was an interactive theorem proving system
for multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990s
to reason about designs for circuits, concurrent algorithms, hardware,
and software ...
(LP).
See also
*
Formal methods
References
External links
*
CASL, The Common Algebraic Specification Language
{{Prog-lang-stub
Formal specification languages