Section 2 of 7 - Prev - Next
All sections - 1 - 2 - 3 - 4 - 5 - 6 - 7

uses dynamic logic as its fundamental semantics (see [Feijs-Jonkers92],
Section 5.9). In COLD-K one can also write algorithmic descriptions, and can
mix algebraic, algorithmic, and dynamic logic specifications. COLD-K has
relatively more sophisticated mechanisms for framing (see [Feijs-Jonkers92],
p. 126, and [Jonkers91]) than most Larch family BISLs (see section 4.9 What
does modifies mean?). All of this would seem to make COLD-K both more
expressive and difficult to learn than a typical Larch family BISL.

1.5 What is the history of the Larch project?

(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. During a programming language workshop
organized by Barbara Liskov, he presented three simple equations relating
operations on sets, and argued that anything that could reasonably be called
a set would satisfy these axioms, and that anything that satisfied these
axioms could reasonably be called a set. John Guttag refined this idea. In
his 1975 Ph.D. thesis (University of Toronto), he showed that all computable
functions over an abstract data type could be defined algebraically using
equations of a simple form. He also considered the question of when such a
specification constituted an adequate definition.

As early as 1974, Guttag and Horning realized that a purely algebraic
approach to specification was unlikely to be practical. At that time, they
proposed a combination of algebraic and operational specifications which
they referred to as "dyadic specification." Working with Wing, by 1980 they
had evolved the essence of the two-tiered approach to specification; the
term "two-tiered" was introduced by Wing in her dissertation [Wing83]. A
description of an early version of the Larch Shared Language was published
in 1983. The first reasonably comprehensive description of Larch was
published in 1985 [Guttag-Horning-Wing85a].

In the spring of 1990, software tools supporting Larch were becoming
available, and people began using them to check and reason about
specifications. To make information on Larch more widely available, it was
decided to write a book [Guttag-Horning93].

The First International Workshop on Larch, organized by Ursula Martin and
Jeannette Wing, was held in Dedham, Massachusetts, July 13-15, 1992
[Martin-Wing93].

1.6 What is the origin of the name Larch?

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. According to Jim, Mike asked John to "think up a new name
quick, because he could just imagine what Senator Proxmire would say if he
noticed that DARPA was sponsoring `a bicycle project' at MIT." John was, he
says, "looking at a larch tree at" his "parent's house" and came up with
"Larch". He also says "I did grow up in Larchmont, and I'm sure that
influenced my choice of name." Jim adds, "It was only later that Butler
Lampson suggested that we could use it for the specification of very `larch'
programs."

The "Larch" is the common name of a species of fir tree. The cover of
[Guttag-Horning93] has a picture of Larch trees on it. For more pictures of
Larch trees, see the following URL.

  http://www.cs.iastate.edu/~leavens/larch-pics.html

GIF format pictures of the Larch logo, can be found at the following URLs.

  http://www.sds.lcs.mit.edu/spd/larch/pictures/larch.gif
  http://www.sds.lcs.mit.edu/spd/larch/pictures/trees.gif

1.7 Where can I get more information on Larch and Larch languages?

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

You might also want to read the introductory article about the family
[Guttag-Horning-Wing85b], although it is now somewhat dated. You might
(especially if you are an academic) want to also read some of the
proceedings of the First International Workshop on Larch [Martin-Wing93],
which contains several papers about Larch.

The usenet newsgroup `comp.specification.larch' is devoted to Larch. You
might also want to read the newsgroup `comp.specification.misc' for more
general discussions.

There was a mailing list, called "larch-interest," for Larch. However, it
has been discontinued, now that the usenet newsgroup is available. The
archives of this list are available from the following URL.

  http://www.research.digital.com/SRC/larch/larch-interest.archive.html

Other on-line resources can be found through the global home page for Larch
at the following URL.

  http://www.sds.lcs.mit.edu/spd/larch/index.html

Other resources are SRC's Larch home page

  http://www.research.digital.com/SRC/larch/larch-home.html

and Horning's page.

  http://www.star-lab.com/horning/larch.html

This frequently asked questions list (FAQ) is accessible on the world-wide
web in:

   http://www.cs.iastate.edu/~leavens/larch-faq.html

HTML, plain text, postscript, and GNU info format versions are also
available by anonymous ftp at the following URLs.

   ftp://ftp.cs.iastate.edu/pub/larch/larch-faq.html
   ftp://ftp.cs.iastate.edu/pub/larch/larch-faq.txt.gz
   ftp://ftp.cs.iastate.edu/pub/larch/larch-faq.ps.gz
   ftp://ftp.cs.iastate.edu/pub/larch/larch-faq.info.tar.gz

1.8 Is there an object-oriented extension to Larch?

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]).

Another question is: does LSL have extensions that support object-oriented
specification? No, there are none in particular. One could imagine
extensions of LSL with some notion of subsorting, as in OBJ
[Futatsugi-etal85] [Goguen-etal87], but as yet this has not been done.

1.9 What is the use of formal specification and formal methods?

There are endless debates about the use of formal specification and formal
methods. For recent discussions see [Saiedian-etal96]. The following
discussion may help you enter the debate in a reasonable fashion.

First, be sure you know what formal methods are, and what they are good for
[Liskov-Guttag86] [Wing90]. Roughly speaking, formal methods encompass
formalized software design processes, formal specifications, formal
derivation of implementations, and formal verification. You might also want
to look at the following URL for more recent work on formal methods.

    http://www.comlab.ox.ac.uk/archive/formal-methods.html

Formal verification of implementations that were not designed with
verification in mind is impossible in general. Formal verification has been
critiqued as too difficult to justify and manage [DeMillo-Lipton79].
Programs can also only be verified relative to some abstract machine
[Fetzer88]. However, these problems haven't stopped people from trying to
use formal verification to gain an added level of confidence (or to help
find bugs [Garland-Guttag-Horning90] [Tan94]) in software that is very
critical (in terms of safety or business factors). Of course, you can still
use formal methods without doing formal verification.

Several advocates of formal methods have tried to explain formal methods by
debunking the "myths" that surround them [Hall90] [Bowen-Hinchey95]. Bowen
and Hinchey have also given some advice in the form of "commandments" for
good use of formal methods [Bowen-Hinchey95b].

Of the various kinds of formal methods, formal specification (that's where
Larch comes in), seem to be the most useful. At a fundamental level, some
specification is needed for any abstraction (otherwise there is no
abstraction [Liskov-Guttag86]). A specification is useful as a contract
between the implementor and a client of an abstraction (such as a procedure
or a data type). This contract lays out the responsibilities and obligations
of both parties, and allows division of labor (and a division of blame when
something goes wrong). However, such a specification need not be formal; the
main reason for preferring formal specification over informal specification
is that formal specification can help prevent the ambiguity and
unintentional imprecision which plague informal specification.

There are, however, some disadvantages to using formal specifications. One
shouldn't take the search for precision to an extreme and try to formalize
everything, as this will probably cost much time and effort. (Instead, try
to formalize just the critical aspects of the system.) Another disadvantage
is that a formal specification can itself contain errors and
inconsistencies, which can lead to the specification becoming meaningless.
The use of formality by itself also does not lead to well-structured and
readable specifications; that is a job that humans have to do.

Although you can use the Larch languages and tools without subscribing to
any particular view on the utility of formal methods, there is an emerging
view of this question in the Larch community. This view is that formal
specification and formal methods are most useful as aids to debugging
designs [Garland-Guttag-Horning90] [Tan94]. The basic idea is that one
writes (what one thinks is) redundant information into specifications, and
this information is compared with the rest of the specification. Often the
supposedly redundant information does not match, and trying to check that it
does brings out design or conceptual errors. Thus formal methods play a role
complementary to prototyping, in that they allow one to analyze certain
properties of a design to see if there are lurking inconsistencies or
problems.

Much of what has been said above seems logical, but experimentation would be
helpful to understand what is really true and to help quantify the costs and
benefits of formal methods.

One last answer to the question: some people find writing formal
specifications (and even proofs) fun. No one knows why.

2. The Larch Shared Language (LSL)

In this chapter, we discuss questions about the Larch Shared Language (LSL).

   * What is the Larch Shared Language (LSL)?
   * Where can I find information on-line about LSL?
   * Where can I get a checker for LSL?
   * Do you have a good makefile to use with the LSL checker?
   * What is a sort?
   * What is the purpose of an LSL trait? What is a trait used for?
   * What are the sections of an LSL trait?
   * What is the difference between assumes and includes?
   * How and when should I use a partitioned by clause?
   * How and when should I use a generated by clause?
   * When should I use an implies section?
   * How and when should I use a converts clause?
   * How and when should I use an exempting clause?
   * What is the meaning of an LSL specification?
   * How does LSL handle undefined terms?
   * Is there support for partial specifications in LSL?
   * Can I define operators using recursion?
   * What pitfalls are there for LSL specifiers?
   * Can you give me some tips for specifying things with LSL?
   * How do I know when my trait is abstract enough?
   * Is there a way to write a trait that will guarantee consistency?
   * Do I have to write all the traits I am going to use from scratch?
   * Where can I find handbooks of LSL traits?
   * How do I write logical quantifiers within an LSL term?
   * Where can I find LaTeX or TeX macros for LSL?
   * How do I write some of those funny symbols in the Handbook in my trait?
   * Is there a literate programming tool for use with LSL?
   * Is there a tool for converting LSL to hypertext for the web?

2.1 What is the Larch Shared Language (LSL)?

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 semantics of LSL is based on classical, multisorted first-order
equational logic (see section 2.14 What is the meaning of an LSL
specification?). However, LSL does have two second-order constructs, which
allow you to specify rules of data type induction and certain kinds of
deduction rules (see section 2.10 How and when should I use a generated by
clause?, and see section 2.9 How and when should I use a partitioned by
clause?).

Unlike a programming language, LSL is a purely declarative, mathematical
formalism. In LSL there are no side-effects, algorithms, etc. (see section
2.18 What pitfalls are there for LSL specifiers?). Instead of specifying
computation, in LSL one specifies mathematical operators and their theories.
These operators are used in Larch behavioral interface specification
languages as their mathematical vocabulary (see section 1.1 What is Larch?
What is the Larch family of specification languages?).

An unusual feature of LSL is that it provides ways to add checkable
redundancy to specifications (see section 2.11 When should I use an implies
section?). See section 1.4 How does Larch compare to other specification
languages?, for more detailed comparisons of LSL and related specification
languages.

See Chapter 4 of [Guttag-Horning93], and the rest of this chapter, for more
information.

2.2 Where can I find information on-line about LSL?

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.3 Where can I get a checker for LSL?, if you don't have the LSL
checker installed on your system.

There is no official reference manual for the latest version of LSL (3.1)
on-line. The defining document for LSL version 2.3 [Guttag-Horning-Modet90]
is available from the URL

  ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-058.ps.gz

2.3 Where can I get a checker for LSL?

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/

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

  ftp://ftp.cs.iastate.edu/pub/larch/

You might also be interested in the Larch Development Environment (LDE),
from Cheng's group at Michigan State University. This environment integrates
tools that support LSL, LP, LCL, and Larch/C++. It runs under SunOS and
Solaris. You can get it from the following URL.

  ftp://ftp.cps.msu.edu/pub/serg/tools/LDE/

2.4 Do you have a good makefile to use with the LSL checker?

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.lp:
        $(LSL) -lp $(LSLFLAGS) $<

checkalltraits:
        $(LSL) $(LSLFLAGS) *.lsl

clean:
        rm -f *.lsl-ckd *.lpfrz
cleanall: clean
        rm -f *.lpscr *.lp *.lplog

If you use the emacs text editor, you can then check your traits by using
M-x compile (and responding with something like checkalltraits and a
return). When you do this, you can then use C-x ` (which is an alias for M-x
next-error) to edit the LSL trait with the next error message (if you're
using a version of the LSL checker version 3.1beta5 or later). Emacs will
put the cursor on the appropriate line for you automatically.

See section 3.10 How do I use LP to check my LSL traits?, for more
information on how to use LP to check the implications in LSL traits.

2.5 What is a sort?

The "sorts" in an LSL trait correspond to the types in a programming
language. They are names for sets of values.

This usage is historical (it seems to come from [Goguen-Thatcher-Wagner78]),
and arises from the desire to avoid the word "type", which is heavily
overused. However, it does have some practical benefit, in that in the
context of a BISL, one can say that a type comes from a programming
language, but a sort comes from LSL.

Unlike some other specification languages (e.g., OBJ [Futatsugi-etal85]
[Goguen-etal87]), in LSL there is no requirement that all sort names be
declared. For example, in the following trait, a sort Answer is used.

AnswerTrait: trait
  introduces
    yes, no, maybe: -> Answer

In summary, LSL sorts are declared by being mentioned in the signatures of
operators.

2.6 What is the purpose of an LSL trait? What is a trait used for?

An 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. (See section 4.4
What is an abstract value?.) Examples include the Integer, Set, Queue, and
String traits in Guttag and Horning's handbook [Guttag-Horning93a]. Another
common use is to specify some function on abstract values, in order to ease
the specification of some procedure.

One might also write a trait in order to:

   * specialize some existing trait by renaming some sorts or by
     instantiating some parameterized sorts,
   * change vocabulary by renaming some operators of some existing trait,
   * state implications, for the benefit of readers, to help debug a
     specification [Garland-Guttag-Horning90], or as input to LP,
   * add additional operators to some existing trait, as a convenience in
     specifying some interface or as a way of introducing a name for some
     idea that is an important concept in an interface specification, or
   * combine several existing traits, to make it easier to use them in an
     interface specification.

2.7 What are the sections of an LSL trait?

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

As a rough guide, one can have the following sections, in the following
order.

   * a context section, consisting of: the several assumes clauses, several
     includes clauses, and several shorthand declarations (enumeration,
     tuple, or union), all of which are optional,
   * several introduces sections (typically zero or one), in which the
     signatures of operators are declared,
   * several asserts sections (typically zero or one), in which various
     properties of operators are specified, and
   * and an optional implies section, in which intended consequences of the
     preceding are specified. The parts of this section are intended to be
     redundant. LP can be used to debug a specification by checking that
     they really follow from the rest of the trait (see [Guttag-Horning93],
     Chapter 7).

A good general introduction is found in [Guttag-Horning93], Chapter 4. See
section 2.8 What is the difference between assumes and includes?, for more
on the purposes of the assumes and includes clauses.

2.8 What is the difference between assumes and includes?

One way to think of this is that includes requests textual inclusion of the
named traits, but assumes only says that all traits that include the trait
being specified must include some trait or traits that makes the assumptions
true. Hence includes is like #include in C or C++, but assumes is quite
different.

A common reason to use assumes instead of includes is when you want to
specify a trait with a sort parameter, and when you also need some operators
to be defined on your sort parameters. For example, Guttag and Horning's
handbook trait Sequence (see [Guttag-Horning93], page 174), starts as
follows

Sequence(E, C): trait
  assumes StrictPartialOrder(>, E)

The assumes clause is used to specify that the sort parameter E must have an
operator > that makes it a strict partial order. One way to view such
assumptions is that they specify what is needed about the theory of a sort
parameter in order to sort check, and make sense of the operators that apply
to the sort parameter [Goguen84] [Goguen86].

One can also use assumes to state assumptions about operators that are trait
parameters. For example, Guttag and Horning's handbook trait Sequence (see
[Guttag-Horning93], page 175), starts as follows.

PriorityQueue (>: E,E -> Bool, E, C): trait
  assumes TotalOrder(E for T)

The assumes clause is used to specify that the parameter >:E,E -> Bool must
make E into a total order.

Another reason to use an assumes clause instead of an includes clause is to
state that a trait is not self-contained, but is intended to be included in
some context in which some other trait has been included. For example,
Guttag and Horning's handbook trait IntegerPredicates (see
[Guttag-Horning93], page 164), starts as follows.

IntegerPredicates (Int): trait
  assumes Integer

The assumes clause is used to specify that this trait has to be used in a
trait that has included (the theory of) the trait Integer.

See [Guttag-Horning93], Section 4.6, for more details.

2.9 How and when should I use a partitioned by clause?

You should use a partitioned by clause to identify (i.e., make equivalent)
some terms that would otherwise be distinct in an LSL trait's theory. A
classic example is in the specification of sets, which includes the
following partitioned by clause (see [Guttag-Horning93], page 166).

  C partitioned by \in

In this example, C is the sort for sets, and \in is the membership operator
on sets. This means that two sets, s1 and s2, are distinct (i.e., not equal)
if there is some element e such that member(e, s1) is not equal to member(e,
s2). Another way to look at this is that, you can prove that two sets are
equal by showing that they have the exactly the same members. (The sets
insert(1, insert(2, {})) and insert(2, insert(1, {})) are thus equal.) This
property is what distinguishes a set from a list, because it says that order
does not matter in a set.

The reason there is a separate clause in LSL for this is because of the
implicit quantifiers involved. The partitioned by clause in the example
above is more powerful than the following (see [Wing95], Section 5.1).

  \forall e: E, s1, s2: Set
     ((e \in s1) = (e \in s2)) => s1 = s2

The reason is that the above code would allow you to conclude that {1,2} =
{2,3}, because both have 2 as a member. (That is, one can let e be 2, and
then the left hand side of the implication holds.) Historically, LSL did not
have a way to write quantifiers inside its formulas, and so the partioned by
clause was necessary. With LSL version 3.1, however, one could write the
following equivalent to the above partitioned by clause for Set. (See
section 2.24 How do I write logical quantifiers within an LSL term?, for the
meaning of \A.)

  \forall e: E, s1, s2: Set
     (\A e (e \in s1) = (e \in s2)) => s1 = s2

However, the above formula will be harder to work with in LP than the
equivalent partitioned by clause. This is because LP has special provision
for using partitioned by clauses. Another reason to prefer the partitioned
by clause is that it conveys intent more clearly than a general logical
formula like the above. Thus it there are still good reasons to use a
partitioned by clause in LSL.

See section 4.2 in Guttag and Horning's book [Guttag-Horning93] for more
details.

2.10 How and when should I use a generated by clause?

You should use a generated by clause to specify that there can be no
abstract values beside the ones that you are describing for a given sort.
This is quite common for specifications of the abstract values of data
types, but will not usually be the case for the abstract values of sort
parameters (such as E in Queue[E]). A generated by clause can also be
thought of as excluding "junk" (i.e., nonstandard values) from a type
[Goguen-Thatcher-Wagner78]. For example, in the trait AnswerTrait (see
section 2.5 What is a sort?), nothing in the specification prevents there
being other elements of the sort Answer besides yes, no, and maybe. That is,
if x has sort Answer, then the formula

    x = yes \/ x = no \/ x = maybe

is not necessarily true; in other words, it's not valid. However, in the
following trait the above formula is valid, because of the generated by
clause. (This is stated in the trait's implies section.)

AnswerTrait2: trait
  includes AnswerTrait
  asserts
    Answer generated by yes, no, maybe
    equations
      yes \neq no;
      yes \neq maybe;
      no \neq maybe;
  implies
    \forall x: Answer
      x = yes \/ x = no \/ x = maybe;

Yet another reason to use a generated by clause is to assert a rule of data
type induction. This view is particularly helpful in LP, because it allows
one to divide up a proof into cases, and to use induction. For example, when
proving some property P(x) holds for all x of sort Answer, the generated by
clause of the trait AnswerTrait2 allows one to proceed by cases; that is, it
suffices to prove P(yes), P(no), and P(maybe).

A more typical induction example can be had by considering Guttag and
Horning's handbook trait Set (see [Guttag-Horning93], page 167). In this
trait, C is the sort for sets. It has the following generated by clause (by
virtue of including the trait SetBasics, see [Guttag-Horning93], page 166).

    C generated by {}, insert

This clause says that the only abstract values of sort C, are those that can
be formed from (finite) combinations of the operators {} and insert. For
example, insert(x, insert(y, {})) is a set. This rules out, for example,
infinite sets, and sets that are nonstandard. It does not say that each such
term denotes a distinct set, and indeed some terms fall in the same
equivalence class (see section 2.9 How and when should I use a partitioned
by clause?). It also does not mean that other operators that form sets
cannot be defined; for example, in the trait Set one can write {x} \U {y}.
What it does say is that every other way to build a set, like this one, has
to be equivalent to some use of {} and insert.

Let us consider a sample proof by structural induction in the trait Set. One
of the implications in this trait is that

  \forall s: C
    size(s) >= 0

To prove this, one must prove that it holds for all sets s. Since, by the
generated by clause, all sets can be formed from {} and insert, it suffices
to prove two cases. For the base case, one must prove the following trivial
result.

    size({}) >= 0

For the inductive case, one gets to assume that

    size(y) >= 0

and then one must prove the following.

  \forall s: C, e: E
    size(insert(e, y)) >= 0

This follows fairly easily; we leave the details to the reader.

See section 4.2 in Guttag and Horning's book [Guttag-Horning93] for more
details on the generated by clause.

One situation where one usually does not want to use a generated by clause
is when specifying the theory of a sort parameter. For example, in the trait
Set (see [Guttag-Horning93], page 167), there is no generated by clause
describing the elements E of the set. The reason not to use a generated by
clause for such sort parameters is to make the assumptions on such
parameters as weak as possible. Thus, unless one has to do induction over
the elements of a sort parameter, one would not need to know that they are
generated.

2.11 When should I use an implies section?

You should usually use an implies section in a trait, even though it adds
nothing to the theory of a trait, and is completely redundant. The reasons
for doing so are as follows.

   * You probably have something interesting to highlight about the theory
     of a trait, to bring to the attention of the reader. This includes
     important examples that help illustrate how to use the operators.
   * You probably have found more than one way to specify something in your
     trait. Putting both of them in the asserts section runs the risk of
     making your theory inconsistent (if they are not really equivalent).
     Leaving one of them out loses information, and prevents possible
     debugging and consistency checking that could otherwise be done (for
     example, using LP; see [Guttag-Horning93], Chapter 7).

Redundancy is a good thing for debugging and consistency checking; after
all, one needs two pieces of information to do any checking.

A motto that mathematicians live by is the following. (You do realize that
writing an LSL trait is doing math, don't you?)

     Few axioms, many theorems.

For LSL, this motto means that you should try to make your asserts section
as small and as elegant as possible, and to push off any redundancy into the
implies section.

An important piece of redundant information you can provide for a reader in
the implies section is a converts clause. You should also consider using a
converts clause for each operator you have introduced in the trait. See
section 2.12 How and when should I use a converts clause?.

Writing a good implies section for a trait is something that takes some
practice. It helps to get a feel for what can be checked with LP first (see
[Guttag-Horning93], Chapter 7). It also helps to look at some good examples;
for example, take a look at the traits in Guttag and Horning's handbook (see
[Guttag-Horning93], Appendix A); most of these have an implies section, and
some are quite extensive.

One general hint about writing implies clauses comes from the fact there are
an infinite number of theorems that follow from every LSL specification.
(One infinite set of theorems concerns the built-in sort Bool.) Since there
are an infinite number of theorems, you can't possibly list all of them.
Focus on the ones that you think are interesting, especially those that will
help the reader understand what your specification is about, and those that
will help you debug your specification.

See Section 4.5 in Guttag and Horning's book [Guttag-Horning93] for more
details.

2.12 How and when should I use a converts clause?

A converts clause goes in the implies section of a trait. It is a way to
make redundant claims about the completeness of the specification of various

Section 2 of 7 - Prev - Next
All sections - 1 - 2 - 3 - 4 - 5 - 6 - 7

© allanswers.org | Terms of use