Larch family: Difference between revisions
Content deleted Content added
Jorge Stolfi (talk | contribs) m Shunted link DEC/SRC |
No edit summary |
||
| Line 1: | Line 1: | ||
The '''Larch family''' of formal [[specification language]]s are intended for the precise specification of computing systems. They allow the clean specification of [[computer program]]s 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]], [[MIT]], and other places. Unlike the [[Z notation]], the Larch family has one language for [[algebraic specification]] 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]], [[C]], [[Smalltalk]], etc.). The Larch project also developed tools to support the use of formal specifications, including LP, the [[Larch Prover]]. |
|||
=== Related Links === |
|||
* [http://www.sds.lcs.mit.edu/spd/larch/ MIT Larch Home Page] |
|||
* [http://www.sds.lcs.mit.edu/spd/larch/pub/larchBook.ps ''Larch: Languages and Tools for Formal Specification''] |
|||
* [http://www.brics.dk/Projects/CoFI/CoFICASL.html CASL, The Common Algebraic Specification Language] |
|||