The Larch Shared Language (LSL) (see [Guttag-Horning93], Chapter 4, and [Guttag-Horning-Modet90]) is a language for specifying mathematical theories. LSL is a kind of equational algebraic specification language [Guttag75] [Guttag-Horning78] [Goguen-Thatcher-Wagner78] [Ehrig-Mahr85] [Futatsugi-etal85] [Mosses96] [Loeckx-Ehrich-Wolf96]. That is, specifications in LSL mainly consist of first-order equations between terms.

The main difference between LSL and a Larch BISL is that in LSL one specifies mathematical theories of the operators that are used in the pre- and postcondition specifications of a Larch BISL. Thus LSL is used to specify mathematical models and auxiliary functions, and the a Larch BISL is used to specify program modules that are to be implemented in some particular programming language.

A good place to start is the Guttag and Horning's book [Guttag-Horning93]. (This book is sometimes called "the silver book" by Larchers.) Consider it required reading. If you find that all tough going, you might want to start with Liskov and Guttag's book [Liskov-Guttag86], which explains the background and motivates the ideas behind abstraction and specification. (See section 1.9 What is the use of formal specification and formal methods?, for more background.

According to Jim Horning (personal communication, January 20, 1998) and John Guttag (personal communication, March 28 1998): "The name was not selected at PARC (hence from the Sunset Western Garden Book), but at MIT. The project had been known informally there as 'Bicycle'." One day Mike Dertouzos [director of the MIT Laboratory for Computer Science] and John were talking on the phone.

You can get the MIT releases of the LSL checker using the world-wide web, starting at the following URL. http://www.sds.lcs.mit.edu/spd/larch/lsl.html You can also get the MIT release by anonymous ftp from the following URL. ftp://ftp.sds.lcs.mit.edu/pub/Larch/LSL/ Iowa State, the Larch/C++ group has made available later beta releases of the LSL checker that fix problems with its profligate use of space. You can get the sources for Unix and Windows 95 executables from the following URL.

Larch [Guttag-Horning93] may be thought of as an approach to formal specification of program modules. This approach is an extension of Hoare's ideas for program specification [Hoare69] [Hoare72a]. Its distinguishing feature is that it uses two "tiers" (or layers) [Wing83]. The top tier is a behavioral interface specification language (BISL), tailored to a specific programming language. Such BISLs typically use pre- and postcondition specifications to specify software modules.

The two "tiers" used in the Larch family of specification languages are LSL, which is called the bottom tier, and a behavioral interface specification language (a BISL), which is called the top tier. This specification of program modules using two "tiers" is a deliberate design decision (see [Wing83] and [Guttag-Horning93], Chapter 3).

Like VDM-SL, Z [Hayes93] [Spivey92] (pronounced "zed") is a specification language that allows both the specification of mathematical values and program modules. Like LSL, Z allows the definition of mathematical operators equationally (see [Spivey92], section 3.2.2). A Z schema is roughly comparable to an LSL trait. The main difference between Z and LSL is that in Z specifications can include state variables.

The following is adapted from a posting of Horning to the larch-interest mailing list on June 19, 1995, which was itself condensed from the preface of [Guttag-Horning93].) This project has been a long time in the growing. The seed was planted by Steve Zilles on October 3, 1973.

This question might mean one of several other more precise questions. These questions are discussed below. One question is: is there a Larch-style BISL for some particular object-oriented (OO) programming language? Yes, there are Larch-style BISLs for Modula-3 (see [Guttag-Horning93], chapter 6, and [Jones91]), Smalltalk-80 (see [Cheon-Leavens94]), and C++ (see [Leavens97] [Leavens96b]).

The Larch Prover (LP) [Garland-Guttag95] is a program that helps check and debug proofs. It is not geared toward proving conjectures automatically, but rather toward automating the tedious parts of proofs. It automates equational rewriting (proofs by normalization), but does not (by default) automatically try other proof techniques. aid the debugging of specifications (i.e.

Besides this FAQ, the best place to look is probably your own computer system. You should have a manual page for the LSL checker, if it's installed on your system. Try the Unix command man lsl to see it. You should also look for a directory (such as '/usr/larch/LSL') where the installation of LSL is found. In that directory, you will find a subdirectory 'Doc', where there is some documentation on the checker. See section 2.

The sections of an LSL trait are determined by the LSL grammar [Guttag-Horning-Modet90]. (See section 2.3 Where can I get a checker for LSL?, for a more recent grammar, which is found in the file 'Doc/lsl3_1.y', for version 3.1, and 'Doc/lsl3_2.y', for version 3.2.

LSL trait denotes a theory, which is a collection of true formulas (of sort Bool). This theory contains "the trait's assertions, the conventional axioms of first-order logic, everything that follows from them, and nothing else" (see [Guttag-Horning93], p. 37). For a brief introduction to these ideas, see Chapter 2 of [Guttag-Horning93]; for general background on equational logic, see [Ehrig-Mahr85] or [Loeckx-Ehrich-Wolf96].

Technically, no; all functions specified in LSL are total (see section 2.14 What is the meaning of an LSL specification?). Thus every operator specified in LSL takes on some value for every combination of arguments. What you can do is to underspecify such an operator, by not specifying what its value is on all arguments. For example, the operator head in the handbook trait List (see [Guttag-Horning93], p. 173) is underspecified in this sense, because no value is specified for head(empty).

No, you don't have to specify everything completely in LSL. It's a good idea, in fact, to only specify the aspects that are important for what you are doing. For example, if you want to reason about graph data structures, it's best to not (at first, anyway) try to specify the theory of graphs in great detail. Put in what you want, and go with that. (This won't hurt anything, because whatever you need to prove you'll be forced to add eventually.

According to Guaspari (posting to the larch-interest mailing list, on March 8, 1995), "the commonest 'purely mathematical' mistakes" in trait definitions occur when one uses structural induction "over constructors that don't freely generate a sort". To understand this, consider his example, which includes the handbook trait Set (see [Guttag-Horning93], page 167).

The first tip helps you write down an algebraic specification of a sort that is intended to be used as an abstract data type (see [Guttag-Horning78], Section 3.4, and [Guttag-Horning93], Section 4.9). The idea is to divide the set of operators of your sort into generators and observers. A constructor returns your sort, while an observer takes your sort in at least one argument and returns some more primitive sort (such as Bool). The tip (quoted from [Guttag-Horning93], p.

The most commonly-used handbook of LSL traits is Guttag and Horning's handbook ([Guttag-Horning93], Appendix A). This can be obtained by anonymous ftp with the LSL checker (see section 2.3 Where can I get a checker for LSL?). A hypertext version is on-line in http://www.research.digital.com/SRC/larch/toc.html A general resource for all known handbooks that are publically available is found on the world-wide web, at the following URL. http://www.cs.iastate.edu/~leavens/Handbooks.

You can get a LaTeX style file, 'larch.sty', and a macro file defining a bunch of mathematical symbols, 'larchmath.tex', by anonymous ftp from the following URL. ftp://ftp.cs.iastate.edu/pub/larch/tex The documentation for 'larch.sty' says that it is to be used with LaTeX 2.09. However, it can be used with LaTeX2e. To do so, put the following lines at the start of your LaTeX input.

Having different BISLs tailored to each programming language allows each BISL to specify all the details of a program module's interface (how to call it) and behavior (what it does). If one has a generic interface specification language, such as VDM-SL [Jones90] [ISO-VDM96] [Fitzgerald-Larsen98], then one cannot specify all interface details. The division into two tiers allows the language used for each tier to be more carefully designed and expressive.

First, a more precise comparison is needed, because Larch is not a single language, but a family of languages (see above). Another problem with this comparison is that Larch has two tiers, but VDM-SL [Jones90] [ISO-VDM96] [Fitzgerald-Larsen98], Z [Hayes93] [Spivey92], and COLD-K [Feijs-Jonkers92] are all integrated languages, which mix aspects of both of the tiers of the Larch family.

By VDM, one means, of course, the specification language VDM-SL [Jones90] [ISO-VDM96] [Fitzgerald-Larsen98]. In comparison with LSL, in VDM-SL one can specify mathematical values (models) using constructs similar to those in denotational semantics and typed, functional programming languages.

Like Larch, COLD-K [Feijs-Jonkers92] makes more of a separation into mathematical and interface specifications, although all are part of the same language. The part of COLD-K comparable to LSL is its algebraic specifications (see [Feijs-Jonkers92], Chapters 2 and 3). In contrast to LSL, COLD-K does not use classical logic, and can specify partial functions. All COLD-K types have an "undefined" element, except the type of the Booleans.

Here is the list of language translations currently in use in 01.com's shared hosting environment, for personal and business: You access these languages by setting the language preference in your web browser, and restarting it prior to accessing the Zimbra interface. Please note that some of these languages are still under development, and should be considered beta. Also note that the 01.

The following makefile shows one way to use the Unix command make to help check LSL traits. It relies on properties of the Bourne shell under Unix and standard Unix make, so it would have to be adjusted to work on other systems. (Also, if you cut and paste this makefile, be sure to change the leading blanks to tab characters on the rule lines.) SHELL = /bin/sh LSL = lsl LSLFLAGS = .SUFFIXES: .lsl .lsl-ckd .lp .lsl.lsl-ckd: $(LSL) $(LSLFLAGS) $< 2>&1 | tee $ .lsl.

LSL trait is used to describe a mathematical theory. This could be used by a mathematician to simply formalize a theory, but more commonly the theory specified is intended to be used as the mathematical vocabulary for some BISL. Another common use is as a way of specifying input to the Larch Prover (LP). When used as mathematical vocabulary for some behavioral interface specification, one can identify some other common uses. Quite often one wants to specify the abstract values of some data type.

The following answer is adapted from a posting to 'comp.specification.larch' by Horning (July 19, 1995) in response to a question by Leavens (July 18, 1995). The trouble starts with your question: there are no "undefined terms" in LSL. LSL is a language of total functions. There are no partial functions associated with operators, although there may be underspecified operators (i.e., operators bound to functions with different values in different models).

In LSL 3.1, you can write a universal quantifier within an LSL term by using \A, and an existential quantifier using \E. As an example, consider the following trait (from Leavens's Math handbook).

Yes, there actually is a version of "spiderweb" specialized for use with LSL. If you are really a fan of such fancy systems, you can find it by using the literate programming library's URL. http://www.desy.de/user/projects/LitProg.html However, we have found that using the "noweb" system is much easier for most people, and nearly as good. You can get noweb from the literate programming library (see above), or directly from the following URL. http://www.eecs.harvard.edu/~nr/noweb/intro.