Internet Info 1997 December/Internet_Info_CD-ROM_Walnut_Creek_December_1997.iso/faqs/comp/answers/larch-faq

Internet Message Format | 1997-10-26 | 202KB

Path: senator-bedfellow.mit.edu!bloom-beacon.mit.edu!howland.erols.net!newsxfer3.itd.umich.edu!newsrelay.iastate.edu!news.iastate.edu!leavens
From: [e-mail] (Gary T. Leavens)
Newsgroups: comp.specification.larch,comp.answers,news.answers
Subject: Larch Frequently Asked Questions (comp.specification.larch FAQ)
Supersedes: <[e-mail]>
Followup-To: comp.specification.larch
Date: 25 Oct 1997 21:16:27 GMT
Organization: Department of Computer Science, Iowa State University
Lines: 4161
Approved: [e-mail]
Distribution: world
Expires: 11/29/97 15:16:03
Message-ID: <[e-mail]>
Reply-To: [e-mail] (Gary T. Leavens)
NNTP-Posting-Host: larch.cs.iastate.edu
Summary: Background on the Larch family of languages,
         including references to where more information can be found.
Keywords: Larch, LSL, LP, BISL, specification, FAQ
X-Content-Currency: This FAQ changes regularly.  When a saved or printed copy
   is over 6 months old, obtain a new one as described in the introduction.
Xref: senator-bedfellow.mit.edu comp.specification.larch:438 comp.answers:28671 news.answers:115330

Posted-By: auto-faq 3.2.1.4
Archive-name: larch-faq
Posting-Frequency: monthly
Version: 1.88
URL: http://www.cs.iastate.edu/~leavens/larch-faq.html
Copyright: (c) 1995, 1996, 1997 Gary T. Leavens
Maintainer: Gary T. Leavens and Matt Markland <[e-mail]>

This FAQ is copyright (C) 1997 Gary T. Leavens.

Permission is granted for you to make copies of this FAQ for educational and
scholarly purposes, and for commercial use in specifying software, but the
copies may not be sold or otherwise used for direct commercial advantage;
permission is also granted to make this document available for file
transfers from machines offering unrestricted anonymous file transfer access
on the Internet; these permissions are granted provided that this copyright
and permission notice is preserved on all copies. All other rights reserved.

----------------------------------------------------------------------------

Larch Frequently Asked Questions

$Revision: 1.88 $

20 October 1997

by Gary T. Leavens

------------------------------------------------------------------------

Table of Contents

   * Introduction
   * Acknowledgements
   * 1 Larch and the Larch Family of Languages
        o 1.1 What is Larch? What is the Larch family of specification
          languages?
        o 1.2 Why does Larch have two tiers?
        o 1.3 What is the difference between LSL and a Larch BISL?
        o 1.4 How does Larch compare to other specification languages?
             + 1.4.1 How does Larch compare to VDM-SL?
             + 1.4.2 How does Larch compare to Z?
             + 1.4.3 How does Larch compare to COLD-K?
        o 1.5 What is the history of the Larch project?
        o 1.6 What is the origin of the name Larch?
        o 1.7 Where can I get more information on Larch and Larch languages?
        o 1.8 Is there an object-oriented extension to Larch?
        o 1.9 What is the use of formal specification and formal methods?
   * 2 The Larch Shared Language (LSL)
        o 2.1 What is the Larch Shared Language (LSL)?
        o 2.2 Where can I find information on-line about LSL?
        o 2.3 Where can I get a checker for LSL?
        o 2.4 Do you have a good makefile to use with the LSL checker?
        o 2.5 What is a sort?
        o 2.6 What is the purpose of an LSL trait? What is a trait used for?
        o 2.7 What are the sections of an LSL trait?
        o 2.8 What is the difference between assumes and includes?
        o 2.9 How and when should I use a partitioned by clause?
        o 2.10 How and when should I use a generated by clause?
        o 2.11 When should I use an implies section?
        o 2.12 How and when should I use a converts clause?
        o 2.13 How and when should I use an exempting clause?
             + 2.13.1 Does exempting some term make it undefined?
             + 2.13.2 How can I exempt only terms that satisfy some
               condition?
        o 2.14 What is the meaning of an LSL specification?
        o 2.15 How does LSL handle undefined terms?
        o 2.16 Is there support for partial specifications in LSL?
             + 2.16.1 Can I specify a partial function in LSL?
             + 2.16.2 Do I have to specify everything completely in LSL?
        o 2.17 Can I define operators using recursion?
        o 2.18 What pitfalls are there for LSL specifiers?
        o 2.19 Can you give me some tips for specifying things with LSL?
        o 2.20 How do I know when my trait is abstract enough?
        o 2.21 Is there a way to write a trait that will guarantee
          consistency?
        o 2.22 Do I have to write all the traits I am going to use from
          scratch?
        o 2.23 Where can I find handbooks of LSL traits?
        o 2.24 How do I write logical quantifiers within an LSL term?
        o 2.25 Where can I find LaTeX or TeX macros for LSL?
        o 2.26 How do I write some of those funny symbols in the Handbook in
          my trait?
        o 2.27 Is there a literate programming tool for use with LSL?
        o 2.28 Is there a tool for converting LSL to hypertext for the web?
   * 3 The Larch Prover (LP)
        o 3.1 What is the Larch Prover (LP)?
        o 3.2 What kind of examples have already been treated by LP?
        o 3.3 How does LP compare with other theorem provers?
        o 3.4 Where can I get an implementation of LP?
        o 3.5 Is there a command reference or list of LP commands?
        o 3.6 Can I change the erase character in LP?
        o 3.7 How do I interrupt LP?
        o 3.8 Do I need to use LSL if I use LP?
        o 3.9 Do I need to use LP if I use LSL?
        o 3.10 How do I use LP to check my LSL traits?
        o 3.11 What is the use of each kind of file generated by the LSL
          checker?
        o 3.12 If LP stops working on my input is it all correct?
        o 3.13 How do I find out where I am in my proof?
        o 3.14 What proof techniques does LP attempt automatically?
        o 3.15 Can you give me some tips on proving things with LP?
        o 3.16 What pitfalls are there for LP users?
        o 3.17 How do I prove that my theory is consistent with LP?
        o 3.18 How can I backtrack if I made a mistake in my proof?
        o 3.19 How do I prove something like 0 <= 2 in LP?
        o 3.20 How can I develop a proof that I can replay later?
        o 3.21 Do I have to reprove everything in an included trait?
        o 3.22 Does LP use assertions in the implies section of an included
          trait?
   * 4 Behavioral Interface Specification Languages (BISLs)
        o 4.1 What is a behavioral interface specification language (BISL)?
        o 4.2 Where can I get a BISL for my favorite programming language?
        o 4.3 Do I need to write an LSL trait to specify something in a
          BISL?
        o 4.4 What is an abstract value?
        o 4.5 What do mutable and immutable mean?
        o 4.6 If I specify an ADT in a BISL do I prove it is the same as the
          trait?
        o 4.7 What does requires mean?
        o 4.8 What does ensures mean?
        o 4.9 What does modifies mean?
        o 4.10 What does trashes mean?
        o 4.11 What does claims mean?
        o 4.12 What is the meaning of a specification written in a BISL?
        o 4.13 How do I specify something that is finite or partial?
        o 4.14 How do I specify errors or error-checking?
        o 4.15 How do I specify that all the values of a type satisfy some
          property?
        o 4.16 What pitfalls are there for BISL specifiers?
        o 4.17 Can you give me some tips for specifying things in a BISL?
   * A Bibliography
   * Footnotes

------------------------------------------------------------------------

Introduction

This document is a draft of a list of frequently asked questions (FAQ) and
their answers for the Larch family of specification languages. It is
intended to be useful to those who are new to Larch, especially to students
and others trying to understand and apply Larch. However, there is some
material that is also intended for experts in other formal methods who would
like to learn more about Larch. If you find something that seems too
technical, please skip a bit, perhaps to another question.

We are looking for more contributions of questions and answers, as well as
corrections and additions to the answers given. Please send e-mail to us at
[e-mail]. We will welcome and acknowledge any help you may
give.

Bibliographic references are described at the end of this document (see
section A Bibliography). They look like "[Wing83]", which give the names of
up to 3 authors, and an abbreviated year of publication.

This FAQ is accessible on the WWW in the following URL.

   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



This FAQ is provided as is without any express or implied warranties. While
every effort has been taken to ensure the accuracy of its information, the
author and maintainers assume no responsibility for errors or omissions, or
for damages resulting from the use of the information contained herein.

Acknowledgements

This work was partially funded by (US) National Science Foundation, under
grant CCR-9503168.

Thanks to Matt Markland who provided the initial impetus for getting this
FAQ started, who helped make up the initial list of questions, and who has
helped edit and maintain it.

Many thanks to John Guttag, Jim Horning, Jeannette Wing, and Steve Garland
for creating the Larch approach and its tools, and for their patient
teaching of its ideas through their writing, personal contact, and many
e-mail messages.

Thanks to Perry Alexander, Al Baker, Eric Eide, Jim Horning, Ursula Martin,
Bertrand Meyer, Clyde Ruby, and Jeannette Wing for general comments and
corrections to this FAQ. Thanks to Steve Garland and Jim Horning for help
with answers. Thanks to Pierre Lescanne, Kishore Dhara, Teo Rus,
Sathiyanarayanan Vijayaraghavan, and Narayanan Sridhar for suggesting
questions.

1 Larch and the Larch Family of Languages

In this chapter, we discuss global questions about Larch.

   * What is Larch?
   * Why does Larch have two tiers?
   * What is the difference between LSL and a Larch BISL?
   * How does Larch compare to other specification languages?
   * What is the history of the Larch project?
   * What is the origin of the name Larch?
   * Where can I get more information on Larch and Larch languages?
   * Is there an object-oriented extension to Larch?
   * What is the use of formal specification and formal methods?

1.1 What is Larch? What is the Larch family of specification languages?

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 bottom tier is the Larch
Shared Language (LSL, see [Guttag-Horning93], Chapter 4), which is used to
describe the mathematical vocabulary used in the pre- and postcondition
specifications. The idea is LSL specifies a domain model, some mathematical
vocabulary, and the BISL specifies both the interface and the behavior of
program modules. See section 1.2 Why does Larch have two tiers?, for more of
the reasons for this separation.

The Larch family of specification languages [Guttag-Horning-Wing85b]
consists of all the BISLs that use LSL for specification of mathematical
vocabulary. Published BISLs with easily accessible references include:

   * Larch/CLU [Wing83] [Wing87], for CLU,
   * Larch/Ada [Guaspari-Marceau-Polak90] [ORA94], for Ada,
   * LCL [Guttag-Horning93] Chapter 5 and [Tan94] [Evans96b], for ANSI C,
   * LM3 [Guttag-Horning93] Chapter 6 and [Jones91] [Jones93], for Modula-3,
   * Larch/Smalltalk [Cheon-Leavens94] [Cheon-Leavens94b], for Smalltalk-80,
   * Larch/C++ [Leavens97] [Leavens96b], for C++, and
   * Larch/ML [Wing-Rollins-Zaremski93], for Standard ML,
   * VSPEC [Baraona-Penix-Alexander95] [Baraona-Alexander96]
     [Baraona-Alexander-Wilsey96], for VHDL.

There are also some BISLs whose documentation is not as easy to come by:
Larch/Generic [Chen89], GCIL (which stands for Generic Concurrent Interface
specification Language [Lerner91]), and Larch/CORBA (a BISL for CORBA IDL
[Sivaprasad95]).

Typically, each BISL uses the declaration syntax of the programming language
for which it is tailored (e.g., C for LCL, Modula-3 for LM3), and adds
annotations to specify behavior. These annotations typically consist of pre-
and postconditions (often using the keywords requires and ensures), some way
to state a frame axiom (often using the keyword modifies), and some way to
indicate what LSL traits are used to provide the mathematical vocabulary.
See section 4 Behavioral Interface Specification Languages (BISLs), for more
details.

1.2 Why does Larch have two tiers?

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). It is
similar to the way that VDM [Jones90] is typically used (one specifies a
model and some auxiliary functions, in a way similar to LSL, and then one
uses that vocabulary to specify the operations that are to be implemented in
some programming language.) However, VDM does not have a family of BISLs
that are tailored to specific programming languages. Only the Larch family,
and the RESOLVE family [Edwards-etal94], have specification languages
tailored to specific programming languages. (See section 1.4 How does Larch
compare to other specification languages?, for more comparisons.)

What are the advantages of using the Larch two-tiered approach?

   * 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]
     [Andrews-etal93], 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. For example, although it is
     possible to deal with finiteness, partiality, exceptional behavior,
     aliasing, mutation, and side-effects in mathematics, dealing with such
     issues requires using more apparatus than just mathematical functions.
     (One might use, for example, the techniques of denotational semantics
     [Schmidt86].) Since such additional apparatus does not fit well with an
     algebraic style of specification, these issues are thus typically
     ignored in LSL specifications. By ignoring these issues, LSL
     specifiations can deal with potentially infinite, pure values, and
     total functions, in a stateless setting. On the other hand, while pre-
     and postcondition specifications are good for the specification of
     finiteness, partiality, exceptions, aliasing, mutation, and
     side-effects, they are not well adapted to the specification of
     mathematical vocabulary. Thus each tier uses techniques that are most
     appropriate to its particular task.
   * The division into two tiers allows the underlying logic to be
     classical. That is, because one is not specifying recursive programs in
     LSL, there is no need for a specialized logic that deals with partial
     functions; instead, LSL can use total functions and classical logic
     [Leavens-Wing97].
   * The domain models described in LSL can be shared among many different
     BISLs, so the effort that goes into constructing such models is not
     limited to just one BISL [Wing83].

One could imagine using some other language besides LSL for the bottom tier
and still getting these advantages. This is done, for example, in RESOLVE
[Edwards-etal94]. Chalin [Chalin95] has suggested that Z [Hayes93]
[Spivey92] could also serve for the bottom tier, but one would probably want
to use a subset of Z without state and the specification of side-effects for
that.

The major disadvantage of the tailoring of each BISL to a specific
programming language is that each BISL has its own syntax and semantics, and
thus requires its own tool support, manuals, etc.

(Parts of the following paragraph are adapted from a personal communication
from Horning of November 29, 1996.)

Something that might seem to be a disadvantage of the Larch approach is that
one sometimes finds oneself writing out a very similar specifications in
both LSL and a BISL. Isn't that a waste of effort? It may seem like that,
but one has to realize that one is doing two different things, and thus the
two similar specifications cannot really be the same. What may happen is
that one writes similar declarations on the two levels, with parallel sets
of operators and procedures. For example, one might specify LSL operators
empty, push, pop, top for stacks, and then specify in a BISL procedures
Empty, Push, Pop, and Top. While the BISL procedure specification will use
the LSL operators in their pre- and postconditions, there will probably be
significant differences in their signatures. For example, the procedure Push
may have a side-effect, rather than returning a new stack value as would the
push operator in the trait. If you find yourself repeating the axioms from
an LSL trait in a BISL specificaton, then you're probably making a mistake.

It is also difficult to extract a simple mathematical vocabulary (like the
total functions of LSL) from a BISL specification. This is because the
semantics of program modules tends to be complex, Thus a BISL specification
is not an appropriate vehicle for the specification of mathematical
vocabulary.

See section 1.3 What is the difference between LSL and a Larch BISL?, for
more discussion on this point.

1.3 What is the difference between LSL and a Larch BISL?

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.

The following summary, provided by Horning (private communication, October
1995), contrasts LSL and a Larch BISL.

  A BISL specifies (not LSL)        LSL specifies (not a BISL)
  ---------------------------       ---------------------------
  State                             Theory definition
    storage allocation              Theory operations
    aliasing, side-effects            inclusion, assumption,
  Control                              implication, parameterization
    errors, exception handling,     Operator definitions
    partiality, pre-conditions,     Facilities for libraries, reuse
    concurrency
  Programming language constructs
    type system, parameter modes,
    special syntax and notations
  Implementation
    (no LSL operators are
     implemented)

Horning's summary is that a BISL handles "all the messy, boring stuff",
while LSL handles "all the subtle, hard stuff", and thus the features in the
two tiers do not overlap much. However, that summary is from the
point-of-view of a designer of LSL. From the point of view of a user of a
Larch BISL, the BISL is where you specify what is to be implemented, and LSL
is where you do "domain modeling".

See [Lamport89] [Guttag-Horning93], Chapter 3, for more about the role of
interface specification, and the separation into two tiers.

1.4 How does Larch compare to other specification languages?

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], Z [Hayes93]
[Spivey92], and COLD-K [Feijs-Jonkers92] are all integrated languages, which
mix aspects of both of the tiers of the Larch family. Thus we will compare
some aspects of VDM-SL and Z to LSL and other aspects to BISLs in the Larch
family (such as LCL or LM3 [Guttag-Horning93], Chapters 5 and 6).

(The comparisons below tend to be a bit technical; if you are not familiar
with specification and verification, you might want to skip to another
question.)

An excellent resource for comparison of LSL to other algebraic specification
languages is [Mosses96]. Also a comparison of Larch with RESOLVE
[Edwards-etal94] is found in [Sitaraman-Welch-Harms93].

   * How does Larch compare to VDM-SL?
   * How does Larch compare to Z?
   * How does Larch compare to COLD-K?

1.4.1 How does Larch compare to VDM-SL?

By VDM, one means, of course, the specification language VDM-SL [Jones90]
[Andrews-etal93]. 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. That is,
one can declare types of records, tagged unions, sets, maps and so on, and
one can specify mathematical functions on such values, either in a
functional style, or by the use of pre- and postcondition specifications.
For example, one might write the following in VDM-SL to define a phone book.

  -- This is a VDM-SL model and auxiliary function specification

  PhoneBook = map Id to (Info | HIDDEN)
  Info :: number : seq of Digit
          address : Address

  listed : PhoneBook * Id -> bool
  listed(pb, id) == id in set dom pb

In the above example, several ASCII approximations to the printed form of
VDM-SL notation are used (e.g., * is an approximation to the glyph for a
cross product, and == is used instead of the definition symbol in the
definition of listed, etc.; see Section 10 of [Andrews-etal93]). The type
PhoneBook is a map to a tagged union type. The type Info is a record type.
The auxiliary function listed is given in a mathematical form, similar to
LSL.

In LSL one can use standard traits (for example, those in Guttag and
Horning's handbook [Guttag-Horning93], Appendix A) and the LSL shorthands
tuple and union (see Section 4.8 of [Guttag-Horning93]) to translate VDM-SL
specifications of mathematical values into LSL. For example, the following
is an approximation to the above VDM-SL specification.

% This is LSL

PhoneBookTrait : trait
  includes Sequence(Digit, Number),
           FiniteMap(PhoneBook, Id, InfoOrHIDDEN)
  Info tuple of number : Number, address : Address
  InfoOrHidden union of left : Info, right : HIDDEN
  introduces
    listed : PhoneBook, Id -> Bool
  asserts
    \forall pb: PhoneBook, id: Id
      listed(pb, id) = defined(pb, id);

However, VDM-SL does not have the equivalent of LSL's equational
specification constructs, and thus it is more difficult in VDM-SL to specify
a mathematical vocabulary at the same level of abstraction. That is, there
is no provision for algebraic specification in VDM-SL.

Because VDM-SL has a component that is like a programming language, and
because it allows recursive definitions, the logic used in VDM-SL is a
three-valued logic instead of the classical, two-valued logic of LSL. This
may make reasoning about VDM-SL specifications relatively more difficult
than reasoning about LSL specifications.

In comparison to Larch family BISLs, the first thing to note is that VDM-SL
is not a BISL itself, as it is not tailored to the specification of
interfaces for some particular programming language. This is evident in the
following example, which continues the above VDM-SL phonebook specification.

  -- The following is a VDM-SL operation specification

  LOOKUP(pb: PhoneBook, id: Id) i: Info
    pre listed(pb, id)
   post i = pb(id)

In the above VDM-SL specification, it is evident that one can define some
generic interface information (parameters, information about their abstract
values, etc.). The pre- and postcondition format of such specifications has
been adopted by most Larch family BISLs. Framing for procedure
specifications in VDM-SL is done by declaring external variables, and noting
which are readable and writable by a procedure; these two classes of
variables are respectively defined by external declarations (in LCL and
Larch/C++), and by the modifies clause. Because VDM-SL is generic, it
cannot, by itself, specify language-specific interface details, such as
pointers, exception handling, etc. However, an advantage of VDM-SL is that
it has better tool support than most BISLs in the Larch family.

1.4.2 How does Larch compare to Z?

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. That is, a Z schema can specify variables, or a
procedure with side effects on such variables. In this respect a Z schema
can act much like a Larch family BISL, since, unlike LSL, it is not
restricted to the specification of mathematical constants and mathematical
functions.

By concentrating on the features of Z that do not involve state variables,
one can more closely compare Z and LSL. We do this for the next several
paragraphs below.

The Z schema calculus (see [Spivey92], section 3.8) allows one to apply to
schemas: most logical connectives, quantification, name hiding, and
pipelining. (One can also use sequential composition between schemas that
specify side-effects.) The schema calculus is thus more expressive than the
LSL mechanisms: includes and assumes. However, in LSL one can effectively
conjoin traits by including them all to make a new trait.

It is possible in Z to write schemas that describe constants and
mathematical functions only. However, many purely mathematical Z schemas
describe something more like an instance of an LSL tuple. This is done in Z
by giving several variable declarations. For example, consider the following
Z schema (in which Z stands for the integers).

  --Z_rational----------------------------------
  | num, den: Z
  ---------------------------------------------

The above is semantically similar to the LSL trait LSL_rational given below.

LSL_rational: trait
  includes Integer
  introduces
    num: -> Int
    den: -> Int

However, in Z usage, the schema Z_rational is likely to be useful, whereas
in LSL one would typically write a trait such as the following, which
specifies a type (called a sort in LSL) of rational numbers.

LSL_rational_sort: trait
  includes Integer
  rational tuple of num: Int, den: Int

The above is semantically similar to a Z schema that defines rational as the
Cartesian product of Z and Z, and specifies the constructors and observers
of the LSL shorthand (see [Guttag-Horning93], Figure 4.10). This is a
difference in usage, not in expressiveness, however.

Z and LSL both have comparable built-in notations for describing abstract
values. Z has basic types (the integers, booleans, etc.) and more type
constructors (sets, Cartesian products, schemas, and free types). A "free
type" in Z (see [Spivey92], Section 3.10) is similar to an LSL union type,
but Z allows direct recursion. Z also has a mathematical tool-kit (see
[Spivey92], Chapter 4) which specifies: relations, partial and total
functions, sequences, and bags, and a large number of operation symbols and
mathematical functions defined on these types. This tool-kit is roughly
comparable to Guttag and Horning's handbook (see [Guttag-Horning93],
Appendix A), although it tends to make heavier use of symbols (like "+")
instead of named functions (like "plus"). (This use of symbols in Z has been
found to be a problem with the understandability of Z specifications
[Finney96]. However, the readability of Z is improved by the standard
conventions for mixing informal commentary with the formal notation.)

LSL and Z both use classical logic, and the underspecification approach to
the specification of partiality, in contrast to VDM-SL. Z does not have any
way of stating the equivalent of an LSL partitioned by or generated by
clause.

See [Baumeister96] for an extended Z example (the birthday book of
[Spivey92]) worked in LSL.

Compared to a Larch family BISL, Z, like VDM-SL is generic, and thus is not
able to specify the interface details of a particular programming language.

An interesting semantic difference between Z and a typical Larch-family BISL
(and VDM-SL) is that Z does not have true preconditions (see [Jackson95],
Sections 7.2 and 8.1); instead, Z has guards (enabling conditions, which are
somewhat like the when clauses of GCIL [Lerner91]). Thus Z may be a better
match to the task of defining finite state machines; the use of enabling
conditions also (as Jackson points out) allows different views of
specifications to be combined. Aside from the Larch BISLs like GCIL that
have support for concurrency, most Larch family BISLs have preconditions
which are "disclaimers". Because of this difference, and the Z schema
calculus, it is much easier to combine Z specifications than it is to
combine specifications in a Larch BISL.

A related point of usage difference is the frequency of the use of
invariants in Z (Spivey calls these "constraints"; see [Spivey92], section
3.2.2). Because in Z one often specifies schemas with state variables, it
makes sense to constrain such variables in various ways. In Z, a common
idiom is to conjoin two schemas, in which case the invariants of each apply
in the conjoined schema. A typical Larch family BISL has no provision for
such conjunction, although object-oriented BISLs (such as Larch/C++) do get
some mileage out of conjunction when subtypes are specified.

Because Z does not distinguish operation specifications from auxiliary
function specifications, it does not have a separation into tiers. So in Z
one can use operations previously specified to specify other operations.

1.4.3 How does Larch compare to COLD-K?

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. The logic in COLD-K has a definedness predicate that allows one to
specify that some term must be undefined, for example; such a specification
is not directly supported by LSL. A feature of COLD-K not found in LSL is
the ability to hide names (see [Feijs-Jonkers92], Section 3.3); that is to
only export certain names from a COLD-K scheme. Both COLD-K and LSL have
mechanisms for importing and renaming.

Compared to a Larch family BISL, COLD-K is often more expressive, because it
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?

At Xerox Palo Alto Research Center, where Jim Horning used to work, the
researchers built many systems, and had to constantly think up new names for
them. They hit on a scheme of always naming systems after plants in a
certain book of plants that occur on the West coast of the US. The "Larch"
is the common name of a species of fir tree that is found in this book.
(Other systems named from this book include "Violet" and "Grapevine".) 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://larch-www.lcs.mit.edu:8001/larch/pictures/larch.gif
  http://larch-www.lcs.mit.edu:8001/larch/pictures/larch-small.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://larch-www.lcs.mit.edu:8001/larch/

Other resources are SRC's Larch home page

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

and Horning's page.

  http://pw1.netcom.com/~jhorning/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://larch-www.lcs.mit.edu:8001/larch/lsl.html

You can also get the MIT release by anonymous ftp from the following URL.

  ftp://larch.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
operators in a trait.

You should consider stating a converts clause for each non-constant operator
you introduce in a trait. If you list an operator in a converts clause, you
would be saying that the operator is uniquely defined "relative to the other
operators in a trait" (see [Guttag-Horning93], p. 142, [Leavens-Wing97],
Section B.1). Of course, this would not be true for every operator you might
define. This means that if you state that an operator is converted in the
implies section of a trait, then you are claiming that there is no ambiguity
in the definition of that operator, once the other operators of the trait
are fixed.

As an example of a converts clause, consider the following trait.

ConvertsExample: trait
  includes Integer
  introduces
    unknown, hmm, known: Int -> Int
  asserts \forall i: Int
    hmm(i) == unknown(i);
    known(i) = i + 1;
  implies
    converts
      known: Int -> Int,
      hmm: Int -> Int

In this trait, the converts clause claims that both known and hmm are
converted. It should be clear that known is converted, because it is
uniquely-defined for all integers. What may be a bit puzzling is that hmm is
also converted. The reason is that once the interpretation of the other
operators in the trait are fixed, in particular once the interpretation of
unknown is fixed, then hmm is uniquely-defined. It would not be correct to
claim that both hmm and unknown are converted; since they are defined in
terms of each other, they would not be uniquely defined relative to the
other operators of the trait.(1)

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

Often one wants to say that some operator is uniquely-defined, but not for
some arguments. This can be done using an exempting clause, which is a
subclause of a converts clause. See section 2.13 How and when should I use
an exempting clause?, for more discussion.

2.13 How and when should I use an exempting clause?

An exempting clause is a subclause of a converts clause. (See section 2.12
How and when should I use a converts clause?.) You should use an exempting
clause when you want to claim that some operator is uniquely-defined,
"relative to the other operators in a trait" ([Guttag-Horning93], p. 142),
except for some special cases.

A very simple example is the trait List (see [Guttag-Horning93], p. 173),
where the converts includes the following.

    converts head
      exempting head(empty)

This just says that head is well-defined, except for taking the head of an
empty list.

A slightly more complicated exempts clause is illustrated by the following
classic example. Suppose one specifies a division operator on the natural
numbers. In such a trait (see [Guttag-Horning93], p. 201), one could use the
following trait outline.

Natural (N): trait
  introduces
    0: -> N
    div: N, N -> N
    % ...
  asserts
    % ...
  implies
    converts div: N, N -> N
      exempting \forall x: N
         div(x, 0)

The converts clause in this example claims that div is uniquely-defined,
relative to the other operators in a trait, except that division by 0 is not
defined. Without the exempting subclause, the converts clause would not be
correct.

See the following subsections and page 44 of [Guttag-Horning93] for more
information.

   * Does exempting some term make it undefined?
   * How can I exempt only terms that satisfy some condition?

2.13.1 Does exempting some term make it undefined?

No, exempting a term does not make it undefined. An exempting clause merely
takes away the claim that it is defined (see [Guttag-Horning93], page 44).
For example, in the trait List (see [Guttag-Horning93], p. 173), writing the
following does not make head(empty) undefined.

    converts head
      exempting head(empty)

If anything, it is the lack of an axiom defining the value of head(empty)
that makes it "undefined". However, you would certainly want to use an
exempting clause in situations where you have a term that is intended to be
"undefined".

The concept of "undefinedness" is a tricky one for LSL. In a technical
sense, nothing is undefined in LSL, because each constant and variable
symbol has a value, and each non-constant operator is a total function (see
[Guttag-Horning93], p. 9, and [Leavens-Wing97], Appendix A). It would be
more accurate to say that in the trait List, the term head(empty) is
"underspecified". This means it has a value, but the trait doesn't specify
what that value is. See section 2.16 Is there support for partial
specifications in LSL?, for more discussion on this point.

2.13.2 How can I exempt only terms that satisfy some condition?

With LSL (through version 3.1) the exempting subclause of a converts clause
is not based on semantics, instead it is based on syntax. You can only
exempt terms having particular forms; these forms allow the arguments to an
operator to be either ground terms (as in head(empty)), or universally
quantified variables or both (as in div(x, 0)).

If you want to exempt all terms for which one argument is positive, or has a
size larger than 3, then you are out of luck. All you can do is to state
your conversion claim informally in a comment (as you can't use a converts
clause naming the operator in question). If you want to rewrite your trait,
you could, for example, change the appropriate argument's sort to be the
natural numbers instead of the integers, or define a new sort for which your
operator is completely-defined.

See Section B.2 of [Leavens-Wing97] for a proposed extension to LSL that
would solve this problem.

2.14 What is the meaning of an LSL specification?

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

Another way to look at the meaning of an LSL trait is the set of models it
denotes. An algebraic model of a trait has a set for each sort, and a total
function for each operator. In addition, it must satisfy the axioms of
first-order logic and the axioms of the trait. A model satisfies an
equational axiom if it assigns the same value to both sides of the equation.
(See [Ehrig-Mahr85], Chapter 1, or [Loeckx-Ehrich-Wolf96], Chapter 5, for
more details.)

In contrast to some other specification languages, the semantics of LSL is
loose (see [Guttag-Horning93], p. 37). That is, there may be several models
of a specification that have observably distinct behavior. For example,
consider the trait ChoiceSet in Guttag and Horning's handbook (see
[Guttag-Horning93], p. 176). There are many models of this trait with
different behavior; for example, it might be that in one model choose({2} \U
{3}) = 2, and in some other model choose({2} \U {3}) = 3. The specification
won't allow you to prove either of these things, of course, because whatever
is provable from the specification is true in all models.

2.15 How does LSL handle undefined terms?

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). The possibility of
     underspecification is intentional; it is important that models of
     traits do not have to be isomorphic.

Another way to say this is that in an algebraic model of a trait (see
section 2.14 What is the meaning of an LSL specification?), each term
denotes an equivalence class, which can be thought of as its definition in
that algebra. In other algebras, the same term may be in a nonisomorphic
equivalence class, if the term is underspecified.

To make this clearer, consider the following trait.

QTrait : trait
  includes Integer
  Q union of theBool: Bool, theInt: Int
  introduces
    isPositive: Q -> Bool
  asserts
    \forall q: Q
      isPositive(q) == q.theInt > 0 /\ (tag(q) = theInt);
  implies
    \forall q: Q, b: Bool
      isPositive(q) == (tag(q) = theInt) /\ q.theInt > 0;
      isPositive(q) == if (tag(q) = theInt)
                       then q.theInt > 0 else false;
      isPositive(theBool(b)) == false;
    converts isPositive: Q -> Bool

In this trait, the question is whether the assertion that defines isPositive
is written correctly. In particular, is isPositive(theBool(true))
"undefined" or an error? This is clarified in the implies section of the
trait, which claims that the order of conjuncts in the definition of
isPositive does not matter, that the definition using if is equivalent, that
the meaning of isPositive(theBool(true)) is false, and that isPositive is
converted (see section 2.12 How and when should I use a converts clause?).

The trait QTrait says that q.theInt is always of sort Int. However, it
places no constraint on what integer it is, unless tag(q) = theInt. So in
the definition and the first implication, both operands of /\ are always
defined (i.e., always mean either true or false, since Bool is generated by
true and false), even though we may not always know which. So the definition
is fine, and the implications are all provable.

The fact that you don't have to use if, and that all the classical laws of
logic (like conjunction being symmetric) apply is a big advantage of the
total function interpretation of LSL. See section 2.16.1 Can I specify a
partial function in LSL? for more discussion.

2.16 Is there support for partial specifications in LSL?

There are two ways one might understand this question. These are dealt with
below.

   * Can I specify a partial function in LSL?
   * Do I have to specify everything completely in LSL?

2.16.1 Can I specify a partial function in LSL?

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). It is a synonym to say that head is
weakly-specified.

One reason LSL takes this approach to dealing with partial functions is that
it makes the logic used in LSL classical. One doesn't have to worry about
non-classical logics, and "bottom" elements of types infecting a term
[Gries-Schneider95]. Another reason is that when LSL is used with a BISL,
the precondition of a procedure specification can protect the operators used
in the postcondition from any undefined arguments [Leavens-Wing97].

(If you want to develop a theory of partial functions, however, you can do
that in LSL. For example, you can specify a type with a constant bottom,
that, for you, represents "undefined". You will just have to manipulate your
partial functions with LSL operators that are total functions.)

2.16.2 Do I have to specify everything completely in LSL?

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

Anything you can specify in LSL, you can do incompletely. (There are no
"theory police" that will check your traits for completeness.) To
incompletely specify a sort, for example, nodes in a graph, just use it's
name in operations and don't say anything more about it. If you need to have
some operators that manipulate nodes, then write their signatures into the
introduces section, but don't write any axioms for them. If you need to know
some properties of these operators, you can write enough axioms in the
asserts section to prove them (perhaps making some of the properties
theorems in the implies section).

The time to worry about the completeness of your theory is when you are
having trouble proving some of the things you want to prove about it, or if
you are preparing it for reuse by others. (On the other hand, a less
complete theory is often more general, so when trying to generalize a trait
for others to use, sometimes it helps to relax some of the properties you
have been working with.)

2.17 Can I define operators using recursion?

Yes, you can define operators recursively. A good, and safe, way to do this
is to use structural induction (e.g., on the generators of a sort). For
example, look at how count is defined in the handbook trait BagBasics (see
[Guttag-Horning93], p. 168). In this trait, the sort C of bags is generated
by the operators {} and insert. There is one axiom that specifies count when
its second argument is the empty bag, and one that specifies count when its
argument is constructed using insert. There are many other examples in the
Guttag and Horning's handbook (see [Guttag-Horning93], Appendix A), for
example the many specifications of operator size (Section A.5), the
specification of the operators head and tail in the trait Queue (p. 171),
the specification of flatten in the trait ListStructureOps (p. 183), and the
specification of operator + in the trait Positive (p. 202). See section 2.19
Can you give me some tips for specifying things with LSL?, for more details
on structural induction.

This kind of recursive specification is so common that if you are familiar
with functional programming (especially in a language like Haskell or ML),
then it's quite helpful to think that way when writing LSL traits.

There is one thing to be careful of, however. Unless you use structural
induction, you might specify an inconsistent trait. The following example
(from David Schmidt, personal communication), illustrates the problem. This
trait includes the Integer trait of Guttag and Horning's handbook (see
[Guttag-Horning93], p. 163).

BadRecTrait: trait
  includes Integer
  introduces
    f: Int -> Int
  asserts
    \forall i: Int
      f(i) == f(i) + 1;

It's easy to prove that this trait is inconsistent; subtract f(i) from both
sides of the defining equation for f, and you obtain 0 = 1. As a heuristic
for avoiding this kind of mistake, avoid recursive specifications that don't
"make progress" when regarded as programs.

It's also possible to fall into a pit when recursively defining a partial
function. The following is a silly example, but illustrates the problem.

BadZeroTrait: trait
  includes Integer, MinMax(Int)
  introduces
    zero: Int -> Int
  asserts
    \forall k: Int
      zero(k) == if k = 0 then 0 else min(k, zero(k-1));

This is silly, the idea being to define a constant function that returns
zero for any nonnegative integer. Still, it looks harmless. However, what
does the specification say about zero(-1). It's easy to see that it's less
than -1, and less than -2, and indeed less than any integer. But the Integer
trait in Guttag and Horning's handbook (see [Guttag-Horning93], p. 163) does
not allow there to be such an integer; so this trait is inconsistent. To
solve this problem, you could change the axiom defining zero to indicate the
intended domain, as follows.

     \forall k: Int
      (k >= 0) => zero(k) = (if k = 0 then 0 else min(k, zero(k-1)));

This revised axiom would allow zero(-1) to have any value. Another cure for
this kind of example would be to specify the domain of zero as the natural
numbers. (Of course, for this particular example, a nonrecursive definition
is also preferable.)

See section 2.18 What pitfalls are there for LSL specifiers?, for another
thing to watch for when making a recursive definition.

2.18 What pitfalls are there for LSL specifiers?

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

GuasparisExample: trait
  includes Integer, Set(Int, Set[Int])

  introduces
    select: Set[Int] -> Int

  asserts
    \forall s: Set[Int], e: Int
      select(insert(e, s)) == e;

  implies
    equations
      insert(1, {2}) == insert(2, {1});
      select(insert(1, {2})) == select(insert(2, {1}));
      1 == 2;  % ouch!

In the above example, the problem with the definition of select is that it's
not well-defined with respect to the equivalence classes of the sort
Set[Int]. The problem is highlighted in the implies section of the trait.
The first implication is a reminder that the order of insertion in a set
doesn't matter; that is, insert(1, {2}) and insert(2, {1}) are equivalent
sets because they have the same members. In the jargon, insert(1, {2}) and
insert(2, {1}) are members of the same equivalence class. The second
implication is a reminder that an operator, such as select must give the
same result on equal arguments; in the jargon, a function must "respect" the
equivalence classes. But the definition of select does not respect the
equivalence classes, because if one applies the definition to both sides of
the second implication, one concludes that 1 = 2.

One way to fix the above definition is shown by the trait ChoiceSet in
Guttag and Horning's handbook (see [Guttag-Horning93], page 176). Another
way that would work in this example (because integers are ordered) would be
to define an operator minimum on the sort Set[Int], and to use that to
define select as follows.

GuasparisExampleCorrected: trait
  includes Integer, Set(Int, Set[Int]), MinMax(Int)

  introduces
    select: Set[Int] -> Int
    minimum: Set[Int] -> Int

  asserts
    \forall s: Set[Int], e, e1, e2: Int
      minimum(insert(e, {})) == e;
      minimum(insert(e1, insert(e2, s)))
        == min(e1, minimum(insert(e2, s)));
      select(insert(e, s)) == minimum(insert(e, s));

  implies
    \forall s: Set[Int], e1, e2: Int
      minimum(insert(e1, insert(e2, s)))
        == minimum(insert(e2, insert(e1, s)));
      select(insert(1, {2})) == 1;
      select(insert(2, {1})) == 1;

To show that minimum is well-defined, one has to prove that it gives the
same answer for all terms in the same equivalence class. The first
implication is this trait does not prove this in general, but does help in
debugging the trait.

To explain the difference that having a "freely-generated" sort makes,
compare the trait GuasparisExample above to the handbook trait Stack (see
[Guttag-Horning93], page 170). In that trait, top is defined using the
following equation.

  \forall e: E, stk: C
    top(push(e, stk)) == e;

Why doesn't this definition have the same problem as the definition of
select? Because it respects the equivalence classes of the sort C (stacks).
Why? Because there is no partitioned by clause for Stack, all equivalence
classes of stacks have a canonical representative. The canonical
representative is a term built using just the operators noted in the
generated by clause for Stack: empty and push; it is canonical because there
is only one way to use just these generators to produce a value in each
equivalence class. The sort of stacks is called freely generated because of
this property. (The sort for sets is not freely generated, because there is
more than one term built using the generators that represents the value
{1,2}.) Since a term of the form push(e, stk) is a canonical representative
of its equivalence class, the specification of top automatically respects
the equivalence classes.

A more involved example is the definition of the set membership operator
(\in) for sets (see [Guttag-Horning93], p. 166 and p. 224). Since sets are
not freely generated, it takes work to prove that the specification of \in
is well-defined. You might want to convince yourself of that as an exercise.

In summary, to avoid this first pitfall, remember the following mantra when
defining operators over a sort with a partitioned by clause or an
interesting notion of equality.

     Is it well-defined?

As a help in avoiding this problem, you can use a freely generated by clause
in the most recent versions of LSL. The use of a freely generated by clause
makes it clear that the reader does not have to be concerned about
ill-defined structural inductions.

Another pitfall in LSL is to assert that all values of some freely-generated
type satisfy some nontrivial property. An example is the trait given below.

BadRational: trait
  includes Integer
  Rational tuple of num: Int, den: Int
  asserts
    \forall r: Rational
       r.den > 0;
  implies
    equations
      ([3, -4]).den > 0;
      (-4) > 0;          % oops!

In this trait, the implications highlight the consequences of this
specification pitfall: an inconsistent theory. The reason the above trait is
inconsistent is that it says that all integers are positive. This is because
for all integers i and j, one can form a tuple of sort rational by writing
[i, j]. This kind of inconsistency arises whenever one has a freely
generated sort, such as LSL tuples, and tries to add constraints as
properties. There are several ways out of this particular pit. The most
straightforward is to use a different sort for the denominators of rationals
(e.g., the positive numbers, as in [Guttag-Horning93], page 207). Another
way is to specify the sort Rational without using a tuple, but using your
own constructor, such as mkRat; this allows the sort to be not freely
generated. The only problem with that approach is that one either has to
make arbitrary or difficult decisions (such as the value of mkRat(3, 0)), or
one has to be satisfied with an underspecified constructor. Another way to
avoid this is to use a parameterized trait; for example, we could have
parameterized BadRational by the sort Int, and instead of including the
trait Integer, used an assumes clause to specify the property desired of the
denominator's sort. In some cases, one can postpone asserting such
properties until one reaches the interface specification; this is because in
a BISL one can impose such properties on variables, not on entire sorts.

To avoid this pit, think of the following mantra.

     Is this property defining a sort, or imposing some constraint on
     another sort?

(If the answer is that it's imposing a constraint on another sort, watch out
for the pit!)

A pitfall that some novices fall into is forgetting that LSL is a purely
mathematical notation, that has no concept of state or side effects. For
example, the following are surely incorrect signatures in LSL.

BadSig: trait
  includes Integer
  introduces
   currentTime: -> Seconds
   random: -> Int

If you think random is a good signature for a random number generator,
you've fallen into the pit. The operator random is an (underspecified)
constant; that is, random stands for some particular integer, always the
same one no matter how many times it is mentioned in an assertion. The
operator currentTime illustrates how mathematical notation is "timeless": it
is also a constant.

How could you specify a notion like a clock in LSL? What you have to do is,
instead of specifying the concept of "the current time", specify the concept
of a clock. For example consider the following trait.

ClockTrait: trait
  assumes TotalOrder(Seconds for T)
  introduces
    newClock: Seconds -> Clock
    tick: Clock -> Clock
    currentTime: Clock -> Seconds
  asserts
    Clock generated by newClock, tick
    \forall sec: Seconds, c: Clock
      currentTime(newClock(sec)) == sec;
      currentTime(tick(c)) > currentTime(c);
  implies
    \forall sec: Seconds, c: Clock
      currentTime(tick(tick(c))) > currentTime(c);

Note that a clock doesn't change state in LSL, however, because each clock
is also timeless, the tick operator produces a new Clock value. Tricks like
this are fundamental to semantics (see, for example, [Schmidt86]). As an
exercise, you might want to specify a random number generator along the same
lines.

To avoid this pit remember the following mantra when you are writing the
signatures of operators in LSL.

     Does this operator have any hidden parameters?

There are no hidden parameters, or global variables, in LSL.

A logical pitfall that one can fall prey of in LSL is failing to understand
that the quantifiers on an equation in LSL are outside the equation as a
whole. Usually this problem can be detected when there is a free variable
that appears only on the right-hand side of an equation. (This assumes that
you use the typical convention of having the right-hand side of an equation
be the "result" of the left-hand side.) For example, consider the following
(from [Wing95], p. 13).

BadSubsetTrait: trait
  includes SetBasics(Set[E] for C)
  introduces
    __ \subseteq __: Set[E], Set[E] -> Bool
  asserts
    \forall e: E, s1, s2: Set[E]
      s1 \subseteq s2 == (e \in s1 => e \in s2);
  implies
    \forall e: E, s1, s2: Set[E]
      (e \in s1 /\ e \in s2) => s1 \subseteq s2;

The implication highlights the problem: if two sets have any single element
in common, then they are considered subsets of each other by the above
trait. This trait could be corrected in LSL by writing the quantifier inside
the defining equation. (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[E]
      s1 \subseteq s2 == \A e (e \in s1 => e \in s2);

This is different, because the right-hand side must hold for all e, not just
some arbitrary e.

To avoid this pit remember the following mantra whenever you use a variable
on only one side of an equation.

     Is it okay if this variable has a single, arbitrary value?

See Wing's paper "Hints to Specifiers" [Wing95] for more tips and general
advice.

2.19 Can you give me some tips for specifying things with LSL?

Yes indeed, we can give you some tips.

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. 54) is to:

     Write an equation defining the result of applying each observer to
     each generator.

For example, consider the following trait.

ResponseSigTrait: trait
  introduces
    yes, no, maybe: -> Response
    optimistic, pessimistic: Response -> Bool
  asserts
    Response generated by yes, no, maybe
    Response partitioned by optimistic, pessimistic

In this trait, the generators are yes, no, and maybe; the observers are
optimistic and pessimistic. What equations would you write?

According to the tip, you would write equations with left-hand sides as in
the following trait. (The tip doesn't tell you what to put in the right hand
sides.)

ResponseTrait: trait
  includes ResponseSigTrait

  asserts
    equations
      optimistic(yes) == true;
      optimistic(no) == false;
      optimistic(maybe) == true;
      pessimistic(yes) == false;
      pessimistic(no) == true;
      pessimistic(maybe) == true;

  implies
    \forall r: Response
      yes ~= no;
      yes ~= maybe;
      no ~= maybe;
      optimistic(r) == r = yes \/ r = maybe;
      pessimistic(r) == r = no \/ r = maybe;

(Defining the operators optimistic and pessimistic as in the last two
equations in the implies section of the above trait is not wrong, but
doesn't follow the tip. That kind of definition can be considered a
shorthand notation for writing down the equations in the asserts section.)

As in the above example, you can specify that some set of generators is
complete by listing them in a generated by clause. If you have other
generators, what Guttag and Horning call extensions, then they can be
defined in much the same way as the observers are defined. As an exercise,
try defining the operator introduced in the following trait.

ResponseTraitExercise: trait
  includes ResponseTrait
  introduces
    negate: Response -> Response

Here are some other general tips for LSL.

   * Try to find a trait that you can reuse before starting to write your
     own trait. Familiarity with Guttag and Horning's handbook
     ([Guttag-Horning93], Appendix A) is very helpful. See section 2.23
     Where can I find handbooks of LSL traits? for other handbooks of
     traits.
   * Break your trait into small pieces. While it's not necessary to do so,
     your traits will be more reusable and more easily understood if they
     are small and focus on a tightly-related set of operators. One
     suggestion is to try to organize your trait as either an ADT (defining
     a sort such as sets, queues, integers, etc.), or as a mixin. A mixin
     trait defines a few operators, or a few properties on operators.
     Examples of mixin traits include all of those in Sections A.10 to A.14
     of [Guttag-Horning93] (such as Associative, Symmetric, TotalOrder, and
     MinMax). A mixin trait typically does not have a generated by or
     partitioned by clause (although the latter sometimes are implied by
     such traits), whereas an ADT trait typically will have at least a
     generated by clause.
   * When writing assertions, think about properties instead of algorithms.
     Since LSL specifications are not executed, you don't have to worry
     about efficiency; instead worry about clarity and correctness. For
     example, when specifying a sort operator, the following is a perfectly
     good idea, even though the implicit algorithm (generate and test) is
     terribly inefficient.

       \forall l1,l2: List[OrderedItem]
         sort(l1) = l2 ==  permutation(l1, l2) /\ ordered(l2);

   * State implications in your traits, and use LP to debug your traits.
     Even if you don't have time to do a lot of this, the mere act of
     thinking about whether what you have written really does imply what you
     think it should will have a beneficial effect on your traits.
   * When you use a negative number in a trait, always put parentheses
     around it. For example, the term -1 < 0 does not parse in LSL unless
     you put parentheses around the -1.

See Wing's paper "Hints to Specifiers" [Wing95] for several more tips and
general advice.

You can also find other tips by looking for the "mottos" and "mantras" in
this chapter. See section 2.18 What pitfalls are there for LSL specifiers?,
for tips on what to avoid.

2.20 How do I know when my trait is abstract enough?

This is a good question, although there's no hard-and-fast answer to it. To
help you in deciding whether a specification is sufficiently abstract, we'll
give you a checklist, and an example of what not to do.

   * Are you using an overly-specific representation?
   * Are you specifying an algorithm for an operator instead of its
     properties?
   * Are you working with an overly-specific sort of data instead of a sort
     parameter and some assumed properties?
   * Are you specifying any unnecessary sizes or other constants?

To illustrate this checklist, we'll give a really awful example of a
specification that isn't abstract enough. It illustrates every fault in the
above list. (Of course, you'd never write anything this bad.)

NonAbstractSet: trait
  includes Integer

  SmallSet tuple of firstDef, secondDef, thirdDef: Bool,
                    first, second, third: Int

  introduces
    {}: -> SmallSet
    insert: Int, SmallSet -> SmallSet
    __ \in __: Int, SmallSet -> Bool
    size: SmallSet -> Int

  asserts
    \forall i,i1,i2,i3: Int, s: SmallSet, b1,b2,b3: Bool
      {} == [false, false, false, 0, 0, 0];

      insert(i, s)
         == if ~s.firstDef
                 then set_first(set_firstDef(s, true), i)
            else if ~s.secondDef
                 then set_second(set_secondDef(s, true), i)
            else if ~s.thirdDef
                 then set_third(set_thirdDef(s, true), i)
            else s;

      i \in s == if s.firstDef /\ i = s.first
                    then true
                 else if s.secondDef /\ i = s.second
                      then true
                 else if s.thirdDef /\ i = s.third
                      then true
                 else false;

      size(s) == if ~s.firstDef then 0
                 else if ~s.secondDef then 1
                 else if ~s.thirdDef then 2
                 else 3;

Comparing this specification with the one in Guttag and Horning's handbook
([Guttag-Horning93], pp. 166-167) reveals a lot about how to write more
abstract specifications. Notice that the trait NonAbstractSet represents the
sort SmallSet as a tuple. This is akin to a "design decision" and makes the
specification less abstract. Another problem is the specification of
algorithms for the observers insert, \in, and size. These could be made more
abstract, even without changing the definition of the sort SmallSet. For
example, using the idea of generators and observers (see section 2.19 Can
you give me some tips for specifying things with LSL?), one could specify
\in as follows.

    i \in {} == false;
    size(s) < 3 => (i \in insert(i, s) = true);

The above trait also defines sets of integers, even though it doesn't
particularly depend on the properties of integers. It would be more abstract
to specify sets of elements. Finally the trait only works for sets of three
elements. Unless there is some good reason for this (for example, modeling
some particular implementation), you should avoid such arbitrary limits in
LSL. They can easily be imposed at the interface level.

Look at traits in the LSL handbook for examples of how to do things right.
You may find that a trait can be too abstract to make it easily understood;
that's fine, you don't have to try to define the ultimate theory of whatever
you're working with.

See [Wing95], section 4.1 for a more extended discussion on the above ideas.
You might want to look at [Liskov-Guttag86] for more background on the
general idea of abstraction in specification. See also [Jones90] for the
related idea of "implementation bias".

2.21 Is there a way to write a trait that will guarantee consistency?

The question of how to write a trait that will guarantee consistency is
important for two reasons.

   * If you use all of LSL, which includes first-order logic, consistency is
     undecidable.
   * If your trait is inconsistent, then for most purposes the theory you
     are specifying is worthless, because everything will be provable (even
     equations such as true == false).

You can trade off ease of expression vs. ease of proving consistency as
follows (quoted from Garland's posting to `comp.specification.larch', June
26, 1996).

     If you are willing to sacrifice ease of proving consistency, you
     can axiomatize your theories in first-order logic, where
     consistency is undecidable.

     If you are willing to sacrifice ease of expression, you can
     achieve consistency as do Boyer and Moore
     [Boyer-Moore79][Boyer-Moore88] with their "principle of
     definition"; that is, you can axiomatize your theories in
     primitive recursive arithmetic rather than in first-order logic.

     If you are willing to settle for some sort of middle ground, and
     you are willing to wait, a future release of the LSL Checker may
     provide some help. I've been thinking about how to enhance the
     checker to provide warnings about potentially inconsistent
     constructions, basically by using a less restrictive version of
     Boyer-Moore principle of definition to classify constructs as safe
     or unsafe.

     Part of my envisioned project for having LSL issue warnings about
     potential inconsistencies involves generating proof obligations
     for LP that can be used to establish consistency when it is in
     doubt.

So you can understand this tradeoff better, and so you can be aware of when
to worry about consistency, we will explain Boyer and Moore's shell
principle and definition principle and how they apply to LSL.

Boyer and Moore's shell principle (see [Boyer-Moore88] Section 2.3 and
[Boyer-Moore79] Section III.E) is a way of introducing new tuple-like sorts;
one would follow it literally in LSL by only using tuple of to construct
sorts. This prevents inconsistency, because it prevents the operators that
construct the new sorts from changing the theory of existing sorts. (That
is, the new theory is a conservative extension of the existing theory; see,
for example, Section 6.12 of [Ehrig-Mahr85].)

Although following the shell principle literally seems far too restrictive
in practice for LSL, one can try to use its ideas to define new sorts in a
disciplined way to help prevent inconsistency. This is done by divide the
set of operators of your sort into generators and observers and specifying
the result of applying each observer to each generator, as described above
(see section 2.19 Can you give me some tips for specifying things with
LSL?). For an example, see the handbook trait SetBasics (in
[Guttag-Horning93], page 166). However, it's not clear whether following
this discipline guarantees that your theory will be consistent.

Boyer and Moore's definition principle (see [Boyer-Moore88] Section 2.6) is
a way of defining auxiliary functions (operators in a trait that are not
generators and that are not the primitive observers used in defining a
sort). The definition principle does not allow one to underspecify a
function; its value must be defined in all of its declared domain.
Furthermore, recursion is only allowed if one can prove that the recursion
is terminating. For LSL this means that a definition of operator f satisfies
the definition principle if it satisfies the following conditions.

   * There is just one equation that defines the operator f, and it has the
     following form, where x1, ..., xn are distinct logical variables,
     called the "formals", and body is an LSL term, called the "body".

     f(x1, ..., xn) == body

   * The only free variables in body are the formals, x1, ..., xn.
   * If the definition is recursive, then the recursion must be proved to
     terminate.

See section 2.17 Can I define operators using recursion?, for how a
nonterminating recursive definition can cause inconsistency.

For examples of what may happen when some of the other conditions of the
definition principle are violated, consider the following trait.

BadDefinitionsTrait: trait
  includes Integer
  introduces
    moreThanOneAxiom: Int -> Bool
    freeVarsInBody: Int -> Int
  asserts
    \forall i, k: Int
      moreThanOneAxiom(i) == i >= 0;
      moreThanOneAxiom(i) == i <= 0;
      freeVarsInBody(i) == k + i;
  implies
    equations
      true == false;
      3 == 2;

The two axioms for the operator moreThanOneAxiom makes the theory
inconsistent; to see this, consider the following calculation.

    true
  = {by the trait Integer}
    4 >= 0
  = {by the first axiom}
    moreThanOneAxiom(4)
  = {by the second axiom}
    4 <= 0
  = {by the trait Integer}
    false

See section 2.18 What pitfalls are there for LSL specifiers?, for the trait
BadRational that illustrates a more subtle way to fall into this kind of
inconsistency.

In the trait BadDefinitionsTrait above, the axiom for freeVarsInBody also
makes the theory inconsistent. This can be seen as follows.

    3
  = {by the trait Integer}
    3 + 0
  = {by the axiom for freeVarsInBody, with k = 3}
    freeVarsInBody(0)
  = {by the axiom for freeVarsInBody, with k = 2}
    2 + 0
  = {by the trait Integer}
    2

See section 2.18 What pitfalls are there for LSL specifiers?, for the trait
BadSig that illustrates another way to fall into this kind of inconsistency.

Because Boyer and Moore's definition principle is quite restrictive, it
should be emphasized that the definition principle does not have to be used
in LSL, and is not even necessary for making consistent definitions. For
example, it seems perfectly reasonable to specify an auxiliary operator by
using several equations, one for each generator of an argument sort (see
section 2.19 Can you give me some tips for specifying things with LSL?),
instead of using just one equation and if then else. The definition
principle requires that all the variables in the defining equation be
distinct, but this seems only to prevent underspecification, not
inconsistency. (See section 2.16.2 Do I have to specify everything
completely in LSL?, for a discussion of underspecification.) The definition
principle also prohibits mutual recursion.

Remember that it's a tradeoff: if you use the definition principle, you are
guaranteed to make consistent auxiliary function definitions, but it may be
harder to specify what you want, and your specifications may be less clear
than they would be otherwise.

See section 3.17 How do I prove that my theory is consistent with LP?, for
how to use LP to help prove that a trait is consistent. This would be useful
if the trait violates either Boyer and Moore's shell principle or the
definition principle.

2.22 Do I have to write all the traits I am going to use from scratch?

No, you don't have to write all the traits you are going to use from
scratch. You should certainly try to use Guttag and Horning's LSL handbook
traits ([Guttag-Horning93], Appendix A), which are freely available. Others
have also made other handbooks available. See section 2.23 Where can I find
handbooks of LSL traits?, for details on how to get these handbooks.

The whole idea of LSL is to enable reuse of traits, so you should
familiarize yourself with the relevant handbooks before starting to write
new traits.

2.23 Where can I find handbooks of LSL traits?

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

Besides a pointer to Guttag and Horning's handbooks, other handbooks found
there include handbooks of: mathematical traits, calendar traits, Larch/C++
traits. There is also a handbook of "SPECS traits", which allows one to
specify in a style similar to VDM-SL. The LSL input for these handbooks can
be obtained from the world-wide web page given above, or by anonymous ftp
from the following URL.

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

2.24 How do I write logical quantifiers within an LSL term?

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

DenseOrder(T) : trait
  includes PartialOrder
  asserts
    \forall x,y,z: T
      (x < y) => (\E z (x < z /\ z < y));
  implies
    \forall x,y,z,t,u: T
      (x < y) => \E z \E t (x < z /\ z < t /\ t < y);
      (x < y) => \E z \E t \E u (x < z /\ z < t /\ t < u /\ u < y);

Note that the variables used in quantifiers are declared before the term.
The variable z used in the asserts section is existentially quantified, and
not universally quantified as might appear from its declaration.

2.25 Where can I find LaTeX or TeX macros for LSL?

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

These files were originally designed by Lamport, and revised by Horning.

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.

\documentclass{article}
\usepackage{larch}

Many published Larch papers and documents have formatting produced by these
TeX macros. However, it's not clear that the use of special symbols is a
good thing. Some of us prefer to let readers see the way the input is typed
(e.g., \in), because we think that non-mathematicians find it easier to
understand words instead of arbitrary symbols. There is some experimental
evidence for this [Finney96], so you might want to think about who your
audience is before you go to a great effort to print fancy symbols in your
specifications.

See section 2.26 How do I write some of those funny symbols in the Handbook
in my trait?.

2.26 How do I write some of those funny symbols in the Handbook in my trait?

The ISO Latin codes for all of the "funny symbols" used in Guttag and
Horning's handbook are found on page 224 of [Guttag-Horning93]. Type the
characters on the right hand side when using LSL. If you are reading the
handbook in print form, you might want to tape a copy of that page to your
wall.

See section 2.25 Where can I find LaTeX or TeX macros for LSL?, for details
on how to get your specification to print out like the handbook.

2.27 Is there a literate programming tool for use with LSL?

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://info.desy.de/user/projects/LitProg.html

(If you don't know what literate programming is, you can find out there as
well.)

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.cs.virginia.edu/~nr/noweb/intro.html

Even easier, it's possible to use the trait modularization facilities of LSL
(includes, and assumes) to use virtually the same style as a literate
programming system would support.

2.28 Is there a tool for converting LSL to hypertext for the web?

Yes, Penix's "lsl2html" tool converts an LSL input file to HTML, so it can
be browsed over the net. It can be found at the following URL.

  http://www.ece.uc.edu/~kbse/lsl2html/

Unfortunately, Penix's tool has a few problems that have never been fixed.
Instead, you might want to use Leavens's tool "lcpp2html", which is
available from the following URL.

  http://www.cs.iastate.edu/~leavens/lcpp2html.html

To use this like "lsl2html" invoke it as follows.

  lcpp2html -P -I *.lsl

3 The Larch Prover (LP)

In this chapter, we discuss questions about the larch prover (LP).

   * What is the Larch Prover (LP)?
   * What kind of examples have already been treated by LP?
   * How does LP compare with other theorem provers?
   * Where can I get an implementation of LP?
   * Is there a command reference or list of LP commands?
   * Can I change the erase character in LP?
   * How do I interrupt LP?
   * Do I need to use LSL if I use LP?
   * Do I need to use LP if I use LSL?
   * How do I use LP to check my LSL traits?
   * What is the use of each kind of file generated by the LSL checker?
   * If LP stops working on my input is it all correct?
   * How do I find out where I am in my proof?
   * What proof techniques does LP attempt automatically?
   * Can you give me some tips on proving things with LP?
   * What pitfalls are there for LP users?
   * How do I prove that my theory is consistent with LP?
   * How can I backtrack if I made a mistake in my proof?
   * How do I prove something like 0 <= 2 in LP?
   * How can I develop a proof that I can replay later?
   * Do I have to reprove everything in an included trait?
   * Does LP use assertions in the implies section of an included trait?

3.1 What is the Larch Prover (LP)?

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.

Although LP is a general proof assistant, its main uses in the context of
Larch are to:

   * aid the debugging of specifications (i.e., theories), by helping
     develop redundant conjectures and their proofs, and
   * checking old proofs in the context of changed theories, to see if the
     proof is still valid.

The philosophy behind LP is "based on the assumption that initial attempts
to state conjectures correctly, and then to prove them, usually fail"
([Garland-Guttag91], page 1). Because of this, LP does not (by default)
automatically attempt steps in a proof that are difficult (i.e.,
speculative, or mathematically interesting). Thus LP does not appear to be a
"smart" assistant in finding proofs; it will not suddenly try a complex
induction by itself. This prevents LP from spending lots of computer time on
conjectures that are not true, and helps make LP predictable. LP can be
thought of more as a "faithful" and "exacting" assistant. This is
appropriate in the debugging stage of a proof, where the steps you should
follow in interacting with LP are as follows.

   * LP applies equational rewriting to your conjecture, and either tells
     you that it's true, or presents you with a subgoal that, if proved,
     will lead to the proof of your conjecture.
   * If you have something left to prove, then ask yourself: "why do I think
     this is true?"
   * If you don't think the current subgoal is true, then you can change
     your conjecture (for example, by strengthening the hypothesis) or your
     theory, and start over.
   * If you think the current subgoal is true, but think you've started the
     proof out the wrong way, then you can backtrack in the proof (by using
     the cancel command).
   * If you think the current subgoal is true, then tell LP to carry out a
     step in the proof that corresponds to your reason. (For example, if you
     believe that the subgoal is true because it's true in each of several
     cases, use the resume by cases command.)
   * LP will then carry out the corresponding proof step for you, and this
     process starts over.

Think of using LP as a game whose prize is certainty about why your
conjecture is true, or at least knowledge about what's wrong with your
theory or conjecture. The main tactical knowledge you need to play the game
well is the correspondence between reasons and proof techniques (see section
3.15 Can you give me some tips on proving things with LP?). Also needed for
good play is the ability to always question the consistency of your theory
and the truth of your conjectures.

The interaction described above is fine for developing conjectures and their
proofs, but LP also has features for replaying proofs, so that you don't
have to interact with it when checking old proofs in slightly modified
settings. See section 3.20 How can I develop a proof that I can replay
later?

See [Guttag-Horning93], Chapter 7, and [Garland-Guttag95] for more
information. See section 3.2 What kind of examples have already been treated
by LP?, for more discussion about the uses of LP.

3.2 What kind of examples have already been treated by LP?

The original reason LP was built to help debug formal specifications (see
[Garland-Guttag-Horning90] and Chapter 7 of [Guttag-Horning93]). It has,
however, also been used for several other purposes, including the following
(reported in messages to the larch-interest mailing list, February 7 and
July 23, 1994).

   * Formal verification of circuits and general reasoning about hardware
     designs (including proofs of invariants, properties, refinement, and
     equivalence between implementations and specifications, see, for
     example, [Saxe-etal92] [Staunstrup-Garland-Guttag89]
     [Staunstrup-Garland-Guttag92]),
   * Reasoning about various mathematical theories, such as relational
     arithmetic and algebra [Martin-Lai92].
   * Verifying sequential programs (such as compilers) or properties of such
     programs.
   * Verification of concurrent programs (such as a distributed multiuser
     service) or properties of concurrent algorithms [Luchangco-etal94]
     [Soegaard-Anderson-etal93]

Several other papers about uses of LP appear in [Martin-Wing93].

3.3 How does LP compare with other theorem provers?

The basic difference between LP and other theorem provers is that LP does
not automatically attempt complex (i.e., interesting or speculative) proof
steps. An additional convenience is that there are tools for supporting the
translation of LSL specifications into LP's input format.

Compared with PVS [Owre-etal95], LP has a less sophisticated user interface,
and less automation. For example, PVS allows one to reorder what lemmas
should be proved more easily. PVS also has decision procedures for ground
linear arithmetic, and possibly better integration of arithmetic with
rewriting. The language used by PVS also has a more sophisticated type
system than does that of LSL (or LP), as it uses predicate subtyping and
dependent types. PVS also provides a strategy language for expressing proof
strategies, although it seems that users typically do not write their own
strategies. On the other hand, LP is more portable (runs on more kinds of
computers), and because its interface does not rely on emacs, it requires
less set-up. Furthermore, as a teaching aid, a less automatic user interface
and a simpler type system have benefits in making students think more.

[[Should discuss NQTHM [Boyer-Moore79][Boyer-Moore88], OTTER, RRL, Isabelle,
and HOL [Gordon-Melham93]. Contributions are welcome here...]]

3.4 Where can I get an implementation of LP?

Currently, LP only runs on Unix machines. You can get an implementation of
LP using the world-wide web, starting at the following URL.

  http://larch-www.lcs.mit.edu:8001/larch/LP/news/distribution.html

You can also get an implementation by anonymous ftp from the following URL.

  ftp://larch.lcs.mit.edu/pub/Larch/lp/

See section 2.3 Where can I get a checker for LSL?, for information about
getting a checker for LSL (that translates LSL traits into LP's input
format), and also for information on the Larch Development Environment
(LDE), that supports LSL, LP, LCL, and Larch/C++.

3.5 Is there a command reference or list of LP commands?

Yes, there is a summary of LP's commands in the section titled "Command
Summary" of [Garland-Guttag95]. For ease of reference, you can find this at
the following URL.

  http://larch-www.lcs.mit.edu:8001/larch/LP/commands/commands.html

(You might want to print this out and paste it on your wall.)

Within an LP process, you can see this by issuing the command help commands.
Use help display to see help on the command display. Use display ? to see
the arguments you can pass to the command display.

3.6 Can I change the erase character in LP?

According to Garland (posting on the larch-interest mailing list, July 14,
1995), the erase (or rubout) character used by LP cannot be changed easily.
The reason is that "LP is written in CLU, and LP's line editing features are
provided by the CLU runtime environment. This environment hard-wires the
delete key [DEL] as the rubout character."

You can erase the current line in LP by typing a C-u (control-U). You can
redisplay the current line by typing C-r. See [Garland-Guttag91], page 7 for
more details.

See section 3.20 How can I develop a proof that I can replay later?, for a
way to avoid tedium and much direct interaction with LP.

If you use emacs, there is a way to get completely around this problem.
Simply start emacs, and type M-x shell, and then run LP from within the Unix
shell that appears. Besides allowing arbitrary editing, this trick allows
you to scroll backwards to view output.

3.7 How do I interrupt LP?

If you are running LP under Unix, the Unix "quit" character (usually C-g,
that's control-g) will interrupt LP's execution.

See section 3.6 Can I change the erase character in LP?, for other
characters that aid in editing interactive input to LP. See section 3.20 How
can I develop a proof that I can replay later?, for a way to avoid tedium
and much direct interaction with LP.

3.8 Do I need to use LSL if I use LP?

No, you do not need to use LSL if you use LP. LP has its own input format
(although it is very similar to LSL's input format). So, many users of LP
simply bypass LSL, and use LP exclusively. On the other hand, using LSL as
an input format to LP has the following advantages.

   * The LSL checker automatically generates proof management commands
     (scripting and logging) for LP, and helps organize theories and
     conjectures into files. See section 3.10 How do I use LP to check my
     LSL traits?.
   * Your theories and conjectures are accessible to a wider audience if
     they are stated in LSL format rather than in LP input format.

3.9 Do I need to use LP if I use LSL?

No, you don't have to use LP if you use LSL. However, it's very helpful to
use LP with LSL, because it aids in debugging LSL traits. The idea is that
you state redundant properties of the theory you are specifying in the
implies section of your LSL trait (see section 2.11 When should I use an
implies section?), and then use LP to check that those really do follow from
the trait. See section 3.10 How do I use LP to check my LSL traits?, and
Chapter 7 of [Guttag-Horning93], for how to do this.

3.10 How do I use LP to check my LSL traits?

There are three main things to check about an LSL trait (see
[Guttag-Horning93], Chapter 7).

   * Is the trait consistent?
   * Do the trait's assumptions (if any) hold?
   * Do the traits implications hold?

The first kind of check is vital, because you can prove anything in an
inconsistent theory. See section 3.17 How do I prove that my theory is
consistent with LP?, and Section 7.6 of [Guttag-Horning93], for more
information on how to do this.

The use of an assumes clause in a trait specifies assumptions about the
context in which that trait is used (see section 2.8 What is the difference
between assumes and includes?); if your trait has included other traits with
assumes clauses, then these assumptions must be checked (see page 124-125 of
[Guttag-Horning93]). However, checking such assumptions is similar to the
checking that happens when checking a trait's implications, which is the
focus of this section.

Here are the top-level steps in using LP to check the implications written
in the implies section of your trait. Let us suppose your trait is called
Foo, and is in a file named `Foo.lsl'.

   * To produce LP input from your trait, you would use the `-lp' switch
     with the LSL checker as follows.

       lsl -lp Foo.lsl

     This produces the following files: `Foo_Axioms.lp', `Foo_Checks.lp',
     and `Foo_Theorems.lp'.
   * Start LP. The suggested name for this command is lp, but on many
     systems it is called LP.

       lp

   * LP will prompt you for input with a prompt that looks like `LP1: '.
     When you see this prompt, type the following.

       execute Foo_Checks

   * LP will read in your input and attempt the first (rewriting) steps of
     the proofs of your conjectures. Often it will suspend each proof
     waiting for your input. See section 3.1 What is the Larch Prover (LP)?,
     for the steps to follow in debugging your trait by trying to prove the
     conjectures in its implies section. See section 3.15 Can you give me
     some tips on proving things with LP? for tips on how to go about a
     proof.

See section 3.20 How can I develop a proof that I can replay later?, for an
alternative to using LP interactively.

See section 3.15 Can you give me some tips on proving things with LP? and
Sections 7.4-7.5 of [Guttag-Horning93], for more information on checking
implications with LP.

3.11 What is the use of each kind of file generated by the LSL checker?

The LSL checker, when used with the `-lp' switch on a file named `Foo.lsl',
in general produces three files: `Foo_Axioms.lp', `Foo_Checks.lp', and
`Foo_Theorems.lp'. Each of these files is in LP input format, hence the
suffix `.lp'.

The file `Foo_Axioms.lp' contains a translation of the trait in `Foo.lsl',
minus the implies section. It is "executed" by LP when LP is executing the
translation of some other LSL trait that includes Foo.

The file `Foo_Checks.lp' contains a translation of the implications in
`Foo.lsl', along with checks of assumptions. As an LP command file, it
starts logging and scripting to the appropriate files (`Foo.lplog' and
`Foo.lpscr'), executes the `Foo_Axioms.lp' file, and then attempts proofs
for each of the checks. This is the main file you execute when using LP.

The file `Foo_Theorems.lp' contains a translation of the implications in
`Foo.lsl', stated as axioms. It is used automatically when it is safe to do
so in the LP input generated by the LSL checker.

All of these files are text files, so viewing them with an editor, or
printing them out, is a good way to solidify your understanding. (See also
page 128 of [Guttag-Horning93].)

3.12 If LP stops working on my input is it all correct?

No, if LP stops working, it may just mean that it wants more guidance from
you. The way to tell if all outstanding conjectures have been proved is to
use the qed command [Garland-Guttag95]. If you see the following, then you
are done.

  All conjectures have been proved.

However, if you see something like the following, then you are not done.

  Still attempting to prove level 2 lemma FooTheorem.2

See section 3.13 How do I find out where I am in my proof?, for a way to
find out what has to be done to finish your proof.

3.13 How do I find out where I am in my proof?

When LP stops reading input from your file (for example, the `_Checks.lp'
file for an LSL trait), the first thing you should do is to get your
bearings. The commands described here also are helpful if you are using LP
interactively, because it's easy to forget what you are trying to do.

To find your bearings, the following commands are helpful (see the section
titled "Sample Proofs: how to guide a proof" in [Garland-Guttag95]).

To find out ...                  Use the command
---------------------------------------------------
What is left to be proved?       display conjectures
What is the status of my proof?  display proof-status
How did I get here?              history
What axioms can I use?           display
What are the current hypotheses? display *Hyp
What are the induction rules?    display induction-rules
What are the deduction rules?    display deduction-rules

The commands display conjectures and display seem to be the most useful.
When you use display conjectures, LP shows where it stopped in your proofs.
There may be several lemmas listed below the first "conjecture". The last of
these (the one with the greatest "level" number) is the one you can work on
first.

See section 3.15 Can you give me some tips on proving things with LP?, for
tips on how to proceed with your proof, once you've found your bearings.

3.14 What proof techniques does LP attempt automatically?

By default, LP automatically uses only the following forward inference
techniques.

   * normalization, and
   * application of deduction rules (that are not inactive).

See section 3.15 Can you give me some tips on proving things with LP?, and
Sections 7.4-7.5 of [Guttag-Horning93], for other proof techniques.

3.15 Can you give me some tips on proving things with LP?

The most important tip for using LP is to think about your conjectures, and
to be very skeptical of their truth.

When you first start using LP, you will be tempted to have it do the
thinking for you. You may find yourself trying random proof techniques to
prove the current subgoal. Resist that temptation! Curb your desire for
automatic proof! Instead, use one of the following two ideas (see the
section titled "Sample Proofs: how to guide a proof" in [Garland-Guttag95]).

Think about whether the conjecture is true, and if so, why you believe it.
(Imagine trying to convince a very skeptical, but logical, person.) If you
believe your conjecture, then your reason may suggest a proof technique.
Here is a small table relating reasons and some of LP's proof techniques.

  If your argument         Then
  has the shape ...        try the following ...
  ------------------------------------------------------
  For a simple case ...,   resume by induction on
    then assuming ...
    for bigger cases...

  On the one hand,         resume by cases ...
    on the other hand...     % or sometimes
                           resume by induction on ...

  If that weren't true,    resume by contradiction
    then ...,                % sometimes followed by
                           critical-pairs *Hyp with *

  By axiom R, ...          apply R to conjecture
                             % or if R contains a free or
                             %    universally quantified variable, x
                           instantiate x by t in R
                             % or if R has an existentially
                             %     quantified variable, x
                           fix x as t in ...

  This should simplify     normalize conjecture with ...
    by ...
                             % or if the ... is a formula
                           rewrite conjecture with ...

Proofs by induction are very common and more useful than you might think.
For example, induction is used to prove the last two implications in
ResponseTrait (see section 2.19 Can you give me some tips for specifying
things with LSL?); in that proof, there are three basis cases, and no
inductive case. This shows that any time you have a generated sort, a proof
by induction can be used, even if there are only a finite number of values
of that sort. Furthermore, you should consider a proof by induction first,
as some other proof techniques (by cases, =>, if-method, contradiction) make
proof by induction more difficult or impossible, because they replace free
variables by constants (see [Garland-Guttag91], page 65).

Another idea is to see if the form of your conjecture suggests a proof
technique. Here is a small table of conjecture forms and proof techniques.
(A name of the form fresh1 is to be replaced by a fresh variable name, that
is, by a name that is not used elsewhere.)

  If your conjecture    Then
  looks like ...        try the following ...
  ------------------------------------------------------
  P1 /\ P2 /\ ...       resume by /\
  P => Q                resume by =>
  P <=> Q               resume by <=>
  if H then P else Q    resume by if-method
  \E x (P(x))           resume by generalizing x from fresh1

If your conjecture looks like \A x (P(x)), then just try whatever method is
suggested for P(x) by itself.

There are some technical caveats for the above suggestions
[Garland-Guttag95]. Using resume by /\ can lead to longer proofs, if the
same lemma is needed in the proof of each conjunct. Using resume by => and
resume by <=> makes certain kinds of proofs by induction impossible (so if
you want to do a proof by induction, do that before using these methods).
The generalization techniques are not helpful if there are other free
variables in the formula.

When all else fails, use the old mathematician's trick of trying to
construct a counterexample to your conjecture. If you can't do it, try to
figure out why you can't (that will suggest a proof technique). Or, if you
start making progress towards a counterexample, keep going. Repeat the
following mantra to yourself.

     It might not be true.

Finally, when you finally succeed in proving your conjecture, don't
celebrate unless you have also shown that your theory is consistent (see
section 3.17 How do I prove that my theory is consistent with LP?).

See section 3.20 How can I develop a proof that I can replay later?, for
advice on how to work noninteractively with LP.

For a short, but important list of tips, see the section titled "Sample
Proofs: how to guide a proof" in [Garland-Guttag95]. See Chapter 7 of
[Guttag-Horning93] for more details.

3.16 What pitfalls are there for LP users?

The biggest pitfall is to not think about what you are doing, but to simply
try random proof strategies. This quickly becomes frustrating. See section
3.15 Can you give me some tips on proving things with LP?, for how to work
with LP in a more fruitful way.

If your theory is inconsistent, proofs may not be easy, but they will always
be possible. Always try to convince yourself of your theory's consistency
before celebrating your proof. See section 3.17 How do I prove that my
theory is consistent with LP?.

3.17 How do I prove that my theory is consistent with LP?

It is difficult to prove a theory is consistent using LP. However, one can
profitably use LP to search for inconsistency. (See section 2.18 What
pitfalls are there for LSL specifiers?, for some common LSL problems that
lead to inconsistency.)

One way to use LP to search for inconsistency is using the complete command.
This directs LP to attempt to add enough rewrite rules to make the theory
equationally complete. If this process finds an inconsistency, such as
proving that true == false, then your theory is inconsistent. (This usually
doesn't stop in an acceptable amount of time and space, but if it does, and
if it hasn't found an inconsistency, and if your theory is purely
equational, then you have proved your theory is consistent.)

Often the completion procedure seems to go off down some path, generating
more and more complex formulas. If this happens, interrupt it (see section
3.7 How do I interrupt LP?) and try using the critical-pairs command to
direct the search for inconsistency by naming two sets (not necessarily
disjoint) of axioms that you wish to deduce consequences of. You can also
use any other of the forward inference techniques in LP (such as the apply
command) to try to deduce an inconsistency in a more directed manner.

See [Guttag-Horning93], section 7.6, for more on this topic. See section
2.21 Is there a way to write a trait that will guarantee consistency?, for a
discussion of the tradeoffs involved between writing an LSL trait in a way
that avoids inconsistency and the difficulty in proving consistency.

3.18 How can I backtrack if I made a mistake in my proof?

If you decide you don't like the way your current proof is going in LP, use
the cancel command to abort the current proof, backtracking to the previous
subgoal. Note that this "suspends work on other proofs until an explicit
resume command is given" [Garland-Guttag95]. See the documentation for
variations of this command.

If you want to start over from scratch, without using the quit command and
restarting LP, use the clear command.

3.19 How do I prove something like 0 <= 2 in LP?

As a way of making the problem of proving things like 0 <= 2 concrete,
consider the following LSL trait. This trait uses the Integer trait in
Guttag and Horning's handbook (see [Guttag-Horning93], p. 163)

DecimalProblem: trait
  includes Integer
  implies
    equations
      ~(1 <= 0);
      0 <= 2;

The problem is how to coax LP into proving these implications. The following
answer is adapted from a posting of Vandevoorde's `comp.specification.larch'
(September 7, 1995).

When the LSL checker translates LSL into LP input, it makes the rewrite
rules for the trait DecimalLiterals (see [Guttag-Horning93], p. 164)
passive, which means that they don't get applied automatically
[Garland-Guttag95]. For example, 2 will not be rewritten to succ(succ(0)).
One reason for this is to keep the conjectures and facts more readable.

However, to prove the implications in your trait, you need to make them
active with the following command.

  make active DecimalLiterals

This is enough to prove ~(1 <= 0) by rewriting. It's also a necessary first
step for the proofs below.

To prove 0 <= 2, you also need to use facts named IsTO* (from the trait
IsTO, see page 194 of [Guttag-Horning93]). The easiest proof to understand
is to instantiate the rule for transitivity as follows.

   instantiate x by 0, y by 1, z by 2 in IsTO.2

(It's a good thing you didn't want to prove 0 <= 9!)

The critical-pairs command is useful for finding such instantiations
automatically. For example, to prove 0 <= 2, you can give the following
commands to LP.

   resume by contradiction    % This turns the (negated) conjecture into
                              % a rewrite rule for critical-pairs.
   critical-pairs *Hyp with * % This is common in contradiction proofs.
                              % For this proof, it suffices to use
                              % critical-pairs *contraHyp with IsTO.4

3.20 How can I develop a proof that I can replay later?

There are probably many ways to develop a proof that you can replay later.
Our technique has the following steps, and starts with an LSL trait. (If you
don't use LSL, you can just use a file of LP input.)

  1. Write a trait Foo into the file `Foo.lsl'.
  2. Use the LSL checker to generate the `Foo_Checks.lp' file.

        % lsl -lp Foo.lsl

  3. Optional: use LP to debug your trait and to try out ideas for proofs of
     the implications interactively.
  4. Copy the file `Foo_Checks.lp' into the file `Foo.proof'.

        % cp Foo_Checks.lp Foo.proof

  5. Optional: if you have used LP already on this trait, then you have a
     head start. There are lines in the `Foo.lpscr' that indicate what to do
     for the proof, and what happened in LP. Copy those lines from the
     `Foo.lpscr' and put them in the `Foo.proof'. For example, after the
     following line in Foo.proof

        prove
          (_x1_ \in _x2_) = (_x1_ \in' _x2_)
          ..

     you might want to add the following lines from the script file. The
     first indicates how you did the proof, and the rest indicate what
     happened.

          resume by induction
             <> basis subgoal
             [] basis subgoal
             <> basis subgoal
             [] basis subgoal
             <> induction subgoal
             [] induction subgoal
          [] conjecture

  6. Optional: if you haven't used LP yet, think about each conjecture, and
     (if you still believe it), after each conjecture, write a LP command
     (or commands) that will complete the proof of that conjecture.
  7. After each conjecture to be proved, following the commands to prove it,
     if any, each list of reasons prove command add the LP command qed. For
     example, your file `Foo.proof', might have a section that looks like
     the following.

        prove
          (_x1_ \in _x2_) = (_x1_ \in' _x2_)
          ..
          resume by induction
             <> basis subgoal
             [] basis subgoal
             <> basis subgoal
             [] basis subgoal
             <> induction subgoal
             [] induction subgoal
          [] conjecture
        qed

  8. Execute the file `Foo.proof' in LP by using the command

       execute Foo.proof

     If this doesn't work, edit the corrections into the file `Foo.proof'.
     Often you can obtain input for this file from the file `Foo.lpscr'.
  9. When your proof executes to completion, use the file `Foo.lpscr' to put
     into `Foo.proof' all of the <> and [] comments that help keep your
     proof synchronized with LP. When you are done, edit `Foo.proof' so that
     the differences with the file `Foo_Checks.lp' are minimal, as shown by
     the following Unix command.

        % diff Foo_Checks.lp Foo.proof | more

One advantage of the above procedure is that you can work on one conjecture
at a time, which allows you to control the order in which the lemmas are
proved. Another advantage is that you tend to think more about what you are
doing than if you are interacting directly with LP. Finally, the above
procedure is quite helpful when, inevitably, you revise your trait.

When you revise your trait, by editing the file `Foo.lsl', use the following
steps to revise your proof.

  1. Use the LSL checker to generate the `Foo_Checks.lp' file for the
     revised trait.

        % lsl -lp Foo.lsl

  2. Use the Unix diff command to check to see what you need to change in
     your proof.

        % diff Foo_Checks.lp Foo.proof | more

     Ignore all the added lines that you put in your proofs such as the
     following.

        78a88,95
        >   resume by induction
        >     <> basis subgoal
        >     [] basis subgoal
        >     <> basis subgoal
        >     [] basis subgoal
        >     <> induction subgoal
        >     [] induction subgoal
        >   [] conjecture
        > qed

     But pay attention to other differences, particularly those for which
     there is a < at the beginning of the line.
  3. Revise your `Foo.proof' file according to the output of the previous
     step, trying to minimize differences as shown by the diff command.
  4. Use LP to rerun your proof. In LP, use the command.

        execute Foo.proof

     If this doesn't work, edit the corrections into the file `Foo.proof'.
     Often you can obtain input for this file from the file `Foo.lpscr'.

3.21 Do I have to reprove everything in an included trait?

No, you should only have to prove that the assumptions from whatever assumes
clauses you have in the included trait hold in your trait. (See pages
124-125 of [Guttag-Horning93].)

3.22 Does LP use assertions in the implies section of an included trait?

According to [Guttag-Horning93] (page 128), LP will reuse the assertions in
the implies section of a trait without forcing you to prove them again "when
it is sound to do so". [[But when is that exactly?]]

4 Behavioral Interface Specification Languages (BISLs)

In this chapter, we discuss questions about Larch Behavioral Interface
Specification Languages (BISLs).

   * What is a behavioral interface specification language (BISL)?
   * Where can I get a BISL for my favorite programming language?
   * Do I need to write an LSL trait to specify something in a BISL?
   * What is an abstract value?
   * What do mutable and immutable mean?
   * If I specify an ADT in a BISL do I prove it is the same as the trait?
   * What does requires mean?
   * What does ensures mean?
   * What does modifies mean?
   * What does trashes mean?
   * What does claims mean?
   * What is the meaning of a specification written in a BISL?
   * How do I specify something that is finite or partial?
   * How do I specify errors or error-checking?
   * How do I specify that all the values of a type satisfy some property?
   * What pitfalls are there for BISL specifiers?
   * Can you give me some tips for specifying things in a BISL?

4.1 What is a behavioral interface specification language (BISL)?

A behavioral interface specification language (BISL) is a kind of
specification language that has the following characteristics.

   * It can specify an exact interface for modules written in some
     particular programming language. For example, Larch/CLU [Wing83]
     [Wing87] can specify the details of how a CLU procedure is called,
     including the types of its arguments, the types of its results, whether
     it is an iterator, and the names and types of exception results.
   * It can specify the behavior of a program module written in that
     programming language. For example, in Larch/CLU one can specify that a
     procedure can signal an exception.

An interface describes exactly how to use a module written in some
programming language. For example, a function declaration in C tells how to
call that function, by giving the function's name, and by describing the
number and types of its arguments.

The concept of behavioral interface specification is an important feature of
the Larch family of specification languages [Wing87]. A particularly good
explanation of the concept of behavioral interface specification is
[Lamport89]. In that paper, Lamport describes a vending machine
specification. To specify a vending machine, it is not sufficient to merely
describe a mathematical mapping between abstract values (money to cans of
soda). One also needs to specify that there will be buttons, a coin slot, a
place for the can of soda to appear, and the meaning of the user interface
events. The buttons, the coin slot, etc. form the interface of the vending
machine; the behavior is described using a mathematical vocabulary that is
an abstraction of the physical machinery that will be used to realize the
specification. The same two pieces are needed to precisely specify a
function to be implemented in, say, C++: the C++ interface information and a
description of its behavior.

Many authors use the term interface specification language for this type of
language. However, there is a natural confusion between this term and an
"interface definition language", such as the CORBA IDL, which merely
specifies interface information and not behavior. To avoid this confusion,
we advocate the term "behavioral interface specification language" for any
language that specifies not only interface information, but also behavior.

In the Larch family there are several BISLs (see section 1.1 What is Larch?
What is the Larch family of specification languages?). In the silver book
[Guttag-Horning93], a Larch BISL is called a "Larch interface language".
However, we do not use the term "Larch interface language" as a synonym for
"BISL", because there are BISLs outside the Larch family (such as those in
the RESOLVE family [Edwards-etal94]). However, "Larch interface language" is
a synonym for "Larch BISL". Another synonym is "Larch interface
specification language".

The first Larch BISL was Larch/CLU [Wing83] [Wing87]. There are now several
others. See section 4.2 Where can I get a BISL for my favorite programming
language?, for information about how to get an implementation.

See section 1.1 What is Larch? What is the Larch family of specification
languages?, and [Guttag-Horning93] for more information.

4.2 Where can I get a BISL for my favorite programming language?

See section 1.1 What is Larch? What is the Larch family of specification
languages? for what Larch BISLs have been discussed in literature and
technical reports. In this section, we concentrate on Larch BISLs that have
some kind of tool support. As far as we know, these are the following.
(Except as noted, the tools are all free.)

LCL  LCL ([Guttag-Horning93], Chapter 5, [Tan94] [Evans96b]) is a BISL for
     ANSI C. Tool support includes LCLint, which can use specification
     information to help find errors in programs. The current implementation
     is available from the following URLs.

       http://larch-www.lcs.mit.edu:8001/larch/lclint/
       ftp://larch.lcs.mit.edu/pub/Larch/lclint/

     There is also a mailing list for LCLint, which you can subscribe to
     using the first URL above, or by sending email to
     [e-mail].
Larch/Ada
     Larch/Ada [Guaspari-Marceau-Polak90] [ORA94] is a BISL for Ada. It is
     part of the specification environment, Penelope, which also has a proof
     assistant and a tool, AdaWise, for checking the subset of Ada used in
     Penelope. AdaWise is free for academic users; for others it can be
     licensed from Oddessy Research Associates (send email to Peter Rukavena
     at [e-mail]). Information on Penelope and AdaWise is
     available at the following URLs.

       http://www.oracorp.com/ada/penelope.html
       http://www.oracorp.com/ada/adawise.html

Larch/Smalltalk
     Larch/Smalltalk [Cheon-Leavens94] [Cheon-Leavens94b] is a BISL for
     Smalltalk-80. It has a syntax and type checker, as well as a
     specification browser. It runs under ParcPlace Objectworks\Smalltalk.
     It can be obtained from the following URLs.

       http://www.cs.iastate.edu/~leavens/larchSmalltalk.html
       ftp://ftp.cs.iastate.edu/pub/larchSmalltalk/

Larch/C++
     Larch/C++ [Leavens97] [Leavens96b] is a BISL for C++. The current
     release has a syntax checker, examples, and a reference manual. It can
     be obtained from the following URLs.

       http://www.cs.iastate.edu/~leavens/larchc++.html
       ftp://ftp.cs.iastate.edu/pub/larchc++/

VSPEC
     VSPEC [Baraona-Penix-Alexander95] [Baraona-Alexander96]
     [Baraona-Alexander-Wilsey96] is a BISL for VHDL. The current release
     has a syntax checker. It can be obtained from the following URLs.

       http://www.ece.uc.edu/~pbaraona/vspec/index.html
       ftp://ftp.ece.uc.edu/pub/users/pbaraona/vspec2.0.tar.gz

GCIL
     The Generic Concurrent Interface Language, GCIL, [Lerner91] has a
     syntax and type checker. It can be obtained from the following URL.

       ftp://ftp.cs.cmu.edu/afs/cs.cmu.edu/project/larch/ftp/gcil.tar.Z

4.3 Do I need to write an LSL trait to specify something in a BISL?

No, you don't always have to write an LSL trait to specify something in a
BISL, it just seems that way. Seriously, you don't have to write a trait in
the following circumstances.

   * You are specifying a procedure and all of the mathematical vocabulary
     needed is available in existing traits. These traits may come from a
     handbook (see section 2.23 Where can I find handbooks of LSL traits?),
     or they may be built-in to your BISL. For example, in most Larch BISLs,
     you would not have to write a trait for your language's built-in
     integer type.
   * Your BISL may create a trait for some compound type for you
     automatically. For example, in LCL, traits are created automatically to
     model C struct types.
   * You have imported a specification file that defines an abstract data
     type (ADT), which is based on an already written trait.

If you are specifying an ADT in a Larch BISL, you will always have to use
some trait to describe its abstract values (see section 4.4 What is an
abstract value?). It might be a trait from a handbook, or some combination
of traits that already exist, but there will have to be one that defines the
abstract values for your ADT.

Note that it is almost always possible to use one of LSL's shorthands or a
combination of handbook traits to specify the abstract values of an ADT. The
only drawback might be that such descriptions of abstract values might not
be as close to your way of thinking about your problem domain as you might
like or it might not have enough high-level vocabulary for your purposes.
For example, when specifying the abstract values of symbol tables, one might
use the handbook trait FiniteMap (see [Guttag-Horning93], page 185).
However, if your symbol table has to handle nested scopes, that trait, by
itself might not be adequate. You might, for example, want to use a stack of
finite maps as abstract values, in which case you might also use the both
the FiniteMap and Stack traits (see [Guttag-Horning93], page 170), and also
add some additional operators to search the abstract values appropriately.
If that kind of thing gets too complex, then it might be better to start
writing your own trait (see section 2.20 How do I know when my trait is
abstract enough?). Also, when using LSL shorthands and standard handbook
traits, be careful that you do not state contradictory constraints as axioms
(see section 2.18 What pitfalls are there for LSL specifiers?).

Usually, when you are specifying a procedure, you won't have to specify a
separate trait, because you will use the vocabulary of the traits that
describe the abstract values of whatever types of arguments and results (and
global variables) your procedure uses. However, if this vocabulary isn't
expressive enough, then you may find it necessary or convenient (see
[Wing95], Section 4.1) to write your own trait. This trait would specify the
additional LSL operators you need to state your procedure's pre- and
postconditions; it would normally assume the traits describing the abstract
values of the procedure's argument and result types (see section 2.8 What is
the difference between assumes and includes?).

The way you tell your BISL what trait it should use differs between BISLs.
For example, in LCL and Larch/C++, the keyword that starts the list of
traits to be used is uses. In Larch/ML, the keyword is using; in Larch/CLU,
it is based on; in LM3 it is TRAITS; in Larch/Smalltalk it is trait, in
Larch/Ada it is TRAIT.

4.4 What is an abstract value?

An abstract value is a mathematical abstraction of some bits that might
exist in your computer. (It's an abstraction in the same sense that a road
map of the United States is an abstraction of the geography and roads of the
United States.) In a Larch BISL's model of your computer, each variable
contains an abstract value. The idea is that, you shouldn't have to reason
about the bit patterns inside the computer, which are mathematically messy,
far removed from the concepts that are important in your problem domain, and
subject to change. Instead, you should reason about your programs using
simple ideas that are close to your problem and independent of the changing
details of your program's data structures.

This idea originated in Hoare's article on specification and verification of
ADTs [Hoare72a]. Hoare's example used an ADT of small integer sets, which
were implemented using arrays, but specified using mathematical sets. The
mathematical sets were thus the abstract values of the arrays used in the
implementation.

See [Liskov-Guttag86] and Chapters 3, 5, and 6 of [Guttag-Horning93] for
more background and information.

4.5 What do mutable and immutable mean?

An object is mutable if its abstract value can change over time. (See
section 4.4 What is an abstract value? for more about abstract values.) For
example, most collection types, such as arrays or records in typical
programming langauges are types with mutable objects.

By contrast, an object is immutable if its abstract value cannot change. For
example, the integers are not mutable, as you cannot change the number 3 to
be 4.

Typically, immutable objects are atomic and do not contain subobjects, while
mutable objects often contain subobjects.

A type with mutable objects is sometimes called an mutable type and a type
with immutable objects is called an immutable type. The specifications of
mutable and immutable types differ in that an immutable type cannot have
operations that mutate objects of that type.

4.6 If I specify an ADT in a BISL do I prove it is the same as the trait?

No, you don't prove the specification of an ADT in a BISL is the same as a
trait. Those are completely different concepts. An LSL trait specifies a
theory, not what is to be implemented in a programming language; the BISL is
what is used to specify an implementation (program module). You use the
vocabulary in a trait to help specify program modules in a BISL, but there
is no proof obligation that you engender by doing so. See section 1.1 What
is Larch? What is the Larch family of specification languages?, and Chapter
3 of [Guttag-Horning93], for more on the general idea of two-tiered
specifications.

What you might want to prove instead is the correctness of an implementation
of your ADT specification; for example, if you specify a class Stack in the
BISL Larch/C++, then you would use an LSL trait to aid the specification
(see section 1.2 Why does Larch have two tiers?), and implement the class in
C++. You could then try to prove that your C++ code is correct with respect
to your Larch/C++ specification. In this proof, you could make use of the
trait's theory. However, you wouldn't be proving any correspondence between
the trait and the BISL specification.

4.7 What does requires mean?

In most Larch BISLs(2), the keyword requires introduces a precondition into
a procedure specification. (This usage dates back to at least Larch/CLU
[Wing83].)

A precondition is a predicate that must hold before a the procedure is
invoked. It documents the obligations of the caller in the contract that is
being specified. Therefore, it can be assumed to be true in an
implementation of the procedure, because if it is does not hold when the
procedure is not obligated to fulfill the contract. This semantics is a
"disclaimer" semantics [Jackson95] [Khosla-Maibaum87]; it differs from an
"enabling condition" semantics, which would mean that the procedure would
not run if called in a state that did not satisfy the precondition.

As an example, consider the specification of a square root function, which
is to be written in C (see [Guttag-Horning93], page 2). In this
specification the precondition is specified by the following line.

  requires x >= 0;

This means that if the value of the formal parameter x is not greater than
or equal to 0, then the specification says nothing about what the
implementation should do. Thus that case does not have to be considered when
writing an implementation.

If the precondition of a procedure is the constant predicate true, the
entire requires clause can usually be omitted. Such procedures can always be
called, and an implementation can make no assumptions about the call except
that the formal parameters will all have whatever types are specified.
Because such a procedure will have to validate any properties it needs from
its arguments, it may be safer in the sense of defensive programming.
However, it may also be slower than one that requires a stronger
precondition, because it will have to spend time validating its arguments.
This is a design tradeoff that can be made either way, but documenting
preconditions in procedure specifications prevents the common performance
problem of having both the caller and the procedure checking the validity of
the arguments. (See [Liskov-Guttag86] for more discussion of this issue.)

A precondition refers to the state just before the specified procedure's
body is run (but after parameter passing). The term comes from Hoare's
original paper on program verification [Hoare69], in which each piece of
program code was described with two predicates: a precondition and a
postcondition. Both the pre- and the postcondition were predicates on states
(that is, they can be considered functions that take a state and return a
boolean). The precondition described the pre-state; that is, it describes
the values of program variables just before the execution of a piece of
code. The postcondition described the post-state, which is the state after
the code's execution. In a Larch BISL the precondition is like this, but the
postcondition is typically a predicate on both the pre- and the post-state.
See section 4.8 What does ensures mean?, for more information.

4.8 What does ensures mean?

In most Larch BISLs, the keyword ensures introduces a postcondition into a
procedure specification. (This usage dates back to at least Larch/CLU
[Wing83].)

A postcondition in a Larch BISL is typically a predicate that is defined on
the pre-state and post-state of a procedure call. (See section 4.7 What does
requires mean?, for background and terminology.) It documents the
obligations of the called procedure in the contract that is being specified.
Therefore, it can be assumed to be true at the end of a call to the
procedure, when reasoning about the call.

As an example, consider the following specification of an integer swap
function which is to be written in C++ (this example is quoted from
[Leavens97]).

extern void swap(int& x, int& y) throw();
//@ behavior {
//@   requires assigned(x, pre) /\ assigned(y, pre);
//@   modifies x, y;
//@   ensures x' = y^ /\ y' = x^;
//@ }

In this specification, the parameters x and y are passed by reference, and
thus each is an alias for a variable in the caller's environment. Because x
and y denote variables, they can have different values in the pre-state and
the post-state. The postcondition of the example above says that the pre-
and post-state values of the variables x and y are exchanged. The notation
x^ refers to the value of x in the pre-state, and x' refers to its value in
the post-state. (This Larch/C++ notation is taken from LCL. In LM3 the ^
notation is not used. In Larch/Smalltalk, the ^ is likewise dropped, and a
subscript "post" is used instead of '.)

Depending on the particular BISL, a procedure specification may have one of
two different interpretations. In most Larch BISLs for sequential
programming languages, the interpretation is that if the precondition holds,
then the procedure must terminate normally in a state where the
postcondition holds. This is called a total correctness interpretation of a
procedure specification. In Hoare's original paper [Hoare69], and in GCIL
and Larch/CORBA, a partial correctness interpretation is used. This means
that if the precondition holds and if the procedure terminates normally,
then the postcondition must hold. You should check the documentation for
your BISL to be sure of its semantics on this point. (Larch/C++ is unique in
that it allows you to specify either interpretation; see [Leavens97],
Chapter 6).

4.9 What does modifies mean?

In most Larch BISLs, the keyword modifies introduces a list of objects that
can be modified by an execution of the specified procedure. (This usage
dates back to Larch/CLU [Wing83].)

An object is modified if its abstract value is changed by the execution of
the specified procedure. (That is, if it has a different abstract value in
the pre-state from the post-state.) Note that the modifies clause does not
mean that the execution must change the object's abstract values; it simply
gives the procedure permission to change them. For example, if a swap
procedure were passed variables with identical values (see section 4.8 What
does ensures mean?, for the specification of swap), then the values would
not be changed.

Note also that a variable's bits may change without a corresponding change
in abstract value (see section 4.4 What is an abstract value?). For example,
if one has a rational number object, whose representation uses two integers.
Let us write the two integers in the representation as (i,j); thus (2,4)
might be one bit pattern that represents the abstract value 1/2. However,
changing the bits from (2,4) to (1,2) would not affect the abstract value.

The modifies clause can be considered syntactic sugar for writing a larger
predicate in the postcondition. Since only the objects listed in the
modifies clause can have their abstract values changed by the execution of
the procedure, all other objects must retain their abstract values. There is
a problem in artificial intelligence called the "frame problem", which is
how to know that "nothing else has changed" when you make some changes to
the world. For this reason, the modifies clause in a Larch BISL can be said
to specify a frame axiom for the specified procedure. See [Borgida-etal95]
for a general discussion of the frame problem for procedure specifications.

In many specification languages, the frame axiom for a procedure
specification is stated in terms of variable names, but in Larch BISLs it is
typically stated in terms of objects. The difference is crucial when the
programming language allows aliasing. If the modifies clause in a Larch BISL
specified that only certain variable names could change their values, then
one would typically need to have either prohibit aliasing completely, or one
would need to write preconditions that prohibited aliases to variables that
were to be modified in procedures.

Mentioning an object in a modifies clause should not give the procedure
being specified permission to deallocate the object. If that were allowed,
it would lead to problems in the BISL's semantics [Chalin95]
[Chalin-etal96]. See section 4.10 What does trashes mean?, for more
information on this topic.

4.10 What does trashes mean?

A trashes clause is similar to a modifies clause (see section 4.9 What does
modifies mean?) in a procedure specification. It gives the procedure
permission to deallocate or trash the objects listed. These objects do not
have to be deallocated or trashed, but no other objects may be deallocated
or trashed.

The notion of trashing an object means that its abstract value should not be
used again. In Larch/C++, allocated variables can be in one of two states:
assigned or unassigned; a variable is unassigned if it has not been assigned
a sensible value. However, if one assigns to an assigned variable, a, the
value of an unassigned variable, then a becomes unassigned, and hence is
considered to be trashed.

Chalin [Chalin95] [Chalin-etal96] pointed out that specification of what a
procedure can modify should be separated from the specification of what it
can deallocate or trash. When these notions are separated, as they are in
Larch/C++ (see [Leavens97], chapter 6), there are two frame axioms for
procedure specifications.

An alternative to a trashes clause, used in LCL, is to specify input/output
modes for formal parameters [Evans96b]. Some parameter modes do not allow
trashing, and some do not allow modification.

4.11 What does claims mean?

The claims clause, and other kinds of checkable redundancy for BISLs, were
introduced into LCL by Tan [Tan94]. In a procedure specification, the
keyword claims introduces a predicate, called a claim, that, like the
postcondition, relates the pre- and post-states of a procedure's execution.
Roughly speaking, the meaning is that the conjunction of the precondition
and the post condition should imply the claim. This implication can be
checked, for example, by using LP.

You could use the claims clause if you wish to highlight some consequences
of your procedure specification for the reader. It can also be used to help
debug your understanding of a procedure specification; for example, if you
think of more than one way to express a postcondition, write all but one way
in a claims clause. Thus the purpose of this clause is similar to the
purpose of the implies section of an LSL trait (see section 2.11 When should
I use an implies section?).

4.12 What is the meaning of a specification written in a BISL?

The exact meaning of a specification in a BISL is, of course, described by
the reference manual for that particular BISL. But in general, the meaning
of a BISL specification is a set of program modules that satisfy the
specification. These program modules are to be written in the programming
language specified. For example, the meaning of a LCL specification is a set
of ANSI C program modules that satisfy the specification. Similarly, the
meaning of a Larch/C++ specification is a set of C++ program modules that
satisfy the specification; a Larch/C++ specification cannot be implemented
in, say, Ada or Modula-3.

How does one describe the satisfaction relation for a BISL? Suppose you want
to describe satisfaction for the BISL Larch/X, whose programs are to be
written in language X. Then you describe the satisfaction relation in at
least the following ways.

   * Give a semantics for language X, that assigns to each program module,
     P, a meaning, M(P). Describe, for each specification, S, written in
     Larch/X, when M(P) is in the set of meanings specified by S.
   * Develop a verification logic for language X, that says how to check
     that code satisfies a specification (or some other specification). Then
     a program module P satisfies a specification S if one can use the
     verification logic to check that P satisfies S.

The first technique will probably allow more programs, in principle, to
satisfy the specification, especially if the semantics of language X covers
all aspects of the language. The second technique is probably more limiting,
but is certainly more useful in practice. These techniques are not mutually
exclusive; for example, a relatively complete verification logic could be
used as a semantics for that language. Furthermore, by using complimentary
definitions of the programming language (e.g., a denotational semantics and
a verification logic), one could prove soundness and completeness results,
which would help debug each kind of semantics, and thus the semantics of the
BISL as well.

See [Wing83] for a semantics of Larch/CLU. See [Jones93] for a semantics of
LM3. See [Tan94] [Chalin95] for semantics of LCL.

4.13 How do I specify something that is finite or partial?

In a procedure specification, you would normally use a precondition to limit
the acceptable arguments that the procedure can work with. For example, the
standard LSL handbook trait Integer (see [Guttag-Horning93], page 163)
specifies an unbounded set of integers. Many Larch BISLs use this kind of
unbounded set of integers as their model of a programming language's
built-in integer type. Suppose that you want to specify an integer
discriminant function, say to be implemented in C++. In Larch/C++ you could
specify this as follows.

extern int discriminant (int a, int b, int c) throw();
//@ behavior {
//@   requires inRange((b * b) - (4 * a * c));
//@   ensures result = (b * b) - (4 * a * c);
//@ }

Notice the precondition; it says that the result must be able to be
represented as an int in the computer (according to the definition of the
operator inRange, which is defined in a built-in trait of Larch/C++
[Leavens97]). Without this precondition, the specification could not be
implemented, because if b were the maximum representable integer, and if a
and c were 0, then the specification without the precondition would say that
the execution would have to terminate normally and return an integer larger
than the maximum representable integer.

(The specification of descriminant above may not be the best design for the
procedure, because it requires a precondition that is difficult to test
without performing the computation specified. See section 4.17 Can you give
me some tips for specifying things in a BISL?, for more discussion of this
point.)

The idea of using preconditions to get around partiality and finiteness
problems in procedures goes back to Hoare's original paper on program
verification [Hoare69].

To specify an ADT with a finite set of values, such as a bounded queue, use
a trait with unbounded values to specify the abstract values. You can then
use an invariant in the BISL specification of your ADT to state that the
size of the abstract values is limited. Most likely the ADT operations that
construct and mutate objects would need to have preconditions that prevent
the abstract value from growing too large. This approach is preferred over
an approach that specifies a finite set of abstract values in LSL, because
that trait would be more complicated and less likely to be able to be reused
(see section 2.20 How do I know when my trait is abstract enough?). Even
with such a trait, you would still need to have preconditions on your
operations that construct and mutate objects, so there is little gained.

4.14 How do I specify errors or error-checking?

Ways of specifying errors and error checking vary between Larch BISLs,
depending primarily on whether the programming language that the BISL is
tailored to has exceptions. In a language without exceptions (like ANSI C),
a procedure would have to signal an error by producing an error message and
halting the program, or by returning some error indication to the caller of
a procedure. If you want to specify that the program halts, most likey you
will just not include the conditions under which it can do so in your
precondition (see section 4.13 How do I specify something that is finite or
partial?). If you want to specify the returning of some error indication (a
return code, etc.), this is done as if you were specifying any other normal
result of a procedure. In a language with exceptions (like C++), there is
the additional option of using the exception handling mechanism to signal
errors to the caller. The syntax of this varies, but typically you will
declare the exceptions as usual for the programming language, and there will
be some special way to indicate in the postcondition that an exception is to
be raised.

Many Larch BISLs (including LCL, LM3, Larch/Ada, and Larch/C++) have special
syntax to support the specification of error checking and signalling
exceptions. However, there is little common agreement among the various
Larch BISLs on the syntax for doing so; please check the manual for your
particular BISL. (See section 1.1 What is Larch? What is the Larch family of
specification languages?, for how to find your language manual.)

See [Liskov-Guttag86] for a discussion of the tradeoffs between using
preconditions and various kinds of defensive programming.

4.15 How do I specify that all the values of a type satisfy some property?

A property that is true for all values of a type is called an invariant.
Many Larch BISLs have syntax for declaring invariants. For example, LM3 uses
the keyword TYPE_INVARIANT, and Larch/C++ uses the keyword invariant. The
predicate following the appropriate keyword has to hold for all objects
having that type, whenever a client-visible operation of that type is called
or returns. (This allows the invariant to be violated temporarily within an
operation implementation.)

Stating an invariant in the BISL specification of an ADT is often preferable
to designing an LSL trait so that the abstract values all satisfy the
property. For example, if you attempt to state such a property as an axiom
in a trait, you can cause the trait to be inconsistent, if the abstract
values of your type are freely generated (see section 2.18 What pitfalls are
there for LSL specifiers?). But invariants in a BISL do not lead to such
inconsistencies, because they describe properties of objects created by an
ADT, not properties of all abstract values.

See section 4.13 How do I specify something that is finite or partial?, for
more discussion about ways to specify that all values of an ADT are finite.

4.16 What pitfalls are there for BISL specifiers?

The main thing to watch out for in a BISL specification is that you don't
specify something that cannot be implemented. It's worth repeating the
following mantra to yourself whenever you write a procedure specification.

     Could I correctly implement that?

Of course, you would never intentionally specify a procedure that cannot be
implemented. So you are only likely to fall into this pit by accident. The
following are some ways it might happen.

A very simple problem is forgetting to write a modifies (or trashes) clause
in a procedure specification when your postcondition calls for some object
to change state (or be deallocated). Remember that leaving out a modifies
clause means that no objects can be modified. Consider the following bad
specification of an increment procedure in Larch/C++. (The formal parameter
i is passed by reference. The throw() says that no exceptions can be thrown.
In the precondition, the term assigned(i, pre) is a technical detail; it
says that i has been previously assigned a value [Leavens97].)

extern void incBad(int& i) throw();
//@ behavior {
//@   requires assigned(i, pre);
//@   ensures i' = i^ + 1;
//@ }

There can be no correct implementation of the above specification, because
the omitted modifies clause does not allow i to be modified, but the
postcondition guarantees that it will be modified. This contradiction
prevents correct implementations.

A more subtle way that your specification might not be implementable is if
you forget to specify a necessary precondition. Suppose we fix the above
specification and produce the following specification of an increment
function. What's wrong now?

extern void incStillBad(int& i) throw();
//@ behavior {
//@   requires assigned(i, pre);
//@   modifies i;
//@   ensures i' = i^ + 1;
//@ }

This specification can't be implemented, because if the pre-state value of i
is the largest int, INT_MAX, then the value INT_MAX+1 can't be stored in it.
So, as specified, there are no correct implementations. Something has to be
done to accommodate the finite range of integers that can be stored in i.
Changing the precondition to be the following would take care of the
problem.

  assigned(i, pre) /\ i^ < INT_MAX

In summary, one thing to watch for is whether you have taken finiteness into
account. See section 4.13 How do I specify something that is finite or
partial?, for more about finiteness considerations in BISL specifications.

Another way that your specification might be unimplementable is if your
stated postcondition contradicts some invariant property (see section 4.15
How do I specify that all the values of a type satisfy some property?) that
you specified elsewhere.

The following is another Larch/C++ example. The term inRange(e), used in the
precondition, means that e is within the range of representable integer
values, hence the specification takes finiteness into account. What else
could be wrong with the specification?

extern void transfer(int& source, int& sink, int amt);
//@ behavior {
//@   requires assigned(source, pre) /\ assigned(sink, pre) /\ amt >= 0
//@            /\ inRange(source^ - amt) /\ inRange(sink^ + amt);
//@   modifies source, sink;
//@   ensures source' = source^ - amt /\ sink' = sink^ + amt;
//@ }

The above specification can't be implemented because it doesn't require that
source and sink not be aliased. Since both source and sink are passed by
reference, suppose that both refer to the same variable i. Then if amt is
nonzero, the postcondition cannot be satisfied. (Suppose the pre-state value
of i is 10, and that amt is 5, then the post-state must satisfy source' = 10
- 5 /\ sink' = 10 + 5, but since both source and sink are aliases for i,
this would require that i' be both 5 and 15, which is impossible.) In
Larch/C++, this could be fixed by adding the following conjunct to the
precondition, which requires that source and sink not be aliased.

  source ~= sink

Some Larch BISLs (e.g., Larch/Ada) prohibit aliasing in client programs, so
if you are using such a BISL, then you don't have to worry about this
particular way of falling in the pit. But if your BISL does not prohibit
aliasing, then you should think about aliasing whenever you are dealing with
mutable objects or call-by-reference.

4.17 Can you give me some tips for specifying things in a BISL?

A basic tip for writing a BISL specification is to try to permit as many
implementations as possible. That is, you want to specify a contract between
clients and implementors that does everything the client needs, but does not
impose any unneeded restrictions on the implementation.

One thing that experienced specifiers think about is whether the
specification permits implementations to be tested. This is particularly
important for preconditions. For example, when specifying an ADT, check that
the ADT has enough operations to allow the pre- and postconditions specified
to be tested. If you specify a Stack ADT but leave out a test for the empty
stack, then it will be impossible for a client to test the precondition of
the pop operation. (However, there are some rare examples, such as a
statistical database, where you might not want to allow clients to have such
access.)

If implementations can be tested, it is often useful to compare the
difficulty in testing the specified precondition with the difficulty of
doing the specified computation. For example, in the specification of
discriminant (see section 4.13 How do I specify something that is finite or
partial?), checking the precondition is likely to be as difficult as the
specified computation. In such a case, it may be wise to change the
specification by weakening the precondition and allowing the procedure to
signal some kind of error or exception.

Another tip is to try to use names for operators in traits that are distinct
from the name of the procedure you are trying to specify (or vice versa).
For example, the casual reader might incorrectly think that the following
specification is recursive.

//@ uses FooTrait;

extern int foo(int input);
//@ behavior {
//@  ensures result = foo(input);
//@ }

There is no logical problem with the above example, since the operators used
in a postcondition cannot have anything to do with the interface procedure
being specified. However, naive readers of specifications are (in our
experience) sometimes confused by such details.

See section 4.16 What pitfalls are there for BISL specifiers?, for pitfalls
to avoid. See [Liskov-Guttag86] [Meyer97] [Meyer92] for general advice on
designing and specifying software. See [Wing95] for some other tips on
formal specification.

A Bibliography

Please send corrections in this bibliography to [e-mail].

[Andrews-etal93]
     D. J. Andrews, et al. Information Technology Programming Languages --
     VDM-SL: First Committee Draft Standard CD1387-1. Document ISO/IEC
     JTC1/SC22/WG19 N-20, November 1993. Available from the URL
     `ftp://gatekeeper.dec.com/pub/standards/vdmsl/'.
[Baraona-Alexander-Wilsey96]
     Phillip Baraona, Perry Alexander, and Philip A. Wilsey. Representing
     Abstract Architectures with Axiomatic Specifications and Activation
     Conditions. Department of Electrical and Computer Engineering and
     Computer Science, PO Box 210030, The University of Cincinnati,
     Cincinnati, OH, April 1996. Available from the URL
     `http://www.ece.uc.edu/~pbaraona/vspec/papers/fmcad96.ps'.
[Baraona-Alexander96]
     Phillip Baraona and Perry Alexander. Abstract Architecture
     Representation Using VSPEC. Department of Electrical and Computer
     Engineering and Computer Science, PO Box 210030, The University of
     Cincinnati, Cincinnati, OH, April 1996. Available from the URL
     `http://www.ece.uc.edu/~pbaraona/vspec/papers/vspec-arch96.ps'.
[Baraona-Penix-Alexander95]
     Phillip Baraona, John Penix, and Perry Alexander. VSPEC: A Declarative
     Requirements Specification Language for VHDL. In J. M. Berge, O. Levia,
     and J. Rouilard (eds.), High-Level System Modeling: Specification
     Languages, pages 51-75. Volume 3 of Current Issues in Electronic
     Modeling (Kluwer Academic Publishers, June 1995).
[Baumeister96]
     Hubert Baumeister. Using Algebraic Specification Languages for
     Model-Oriented Specifications. Technical Report MPI-I-96-2-003,
     Max-Planck-Institut fuer Informatik, February 1996. Available from the
     URL
     `http://www.mpi-sb.mpg.de/~hubert/MPII-96-2-003.html'.
[Borgida-etal95]
     Alex Borgida, John Mylopoulos, and Raymond Reiter. On the Frame Problem
     in Procedure Specifications. IEEE Transactions on Software Engineering,
     21(10):785-798, October 1995.
[Bowen-Hinchey95]
     J. P. Bowen and M. G. Hinchey. Seven More Myths of Formal Methods. IEEE
     Software, 12(4):34-41 (July 1995).
[Bowen-Hinchey95b]
     J. P. Bowen and M. G. Hinchey. Ten Commandments of Formal Methods. IEEE
     Computer, 28(4):56-63 (April 1995).
[Boyer-Moore79]
     Robert S. Boyer and J Strother Moore. A Computational Logic. Academic
     Press, 1979.
[Boyer-Moore88]
     Robert S. Boyer and J Strother Moore. A Computational Logic Handbook.
     Academic Press, 1988.
[Chalin95]
     Patrice Chalin. On the Language Design and Semantic Foundation of LCL,
     a Larch/C Interface Specification Language. PhD thesis, Computer
     Science Department, Concordia University, October 1995. Also Technical
     Report CU/DCS TR 95-12, which can be obtained from the URL
     `ftp://ftp.cs.concordia.ca/pub/chalin/tr.ps.Z'.
[Chalin-etal96]
     Patrice Chalin, Peter Grogono, and T. Radhakrishnan. Identification of
     and solutions to shortcomings of LCL, a Larch/C interface specification
     language. In Marie-Claude Gaudel and James Woodcock (eds.), FME'96:
     Industrial Benefit and Advances in Formal Methods, pages 385-404.
     Volume 1051 of Lecture Notes in Computer Science, Springer-Verlag,
     1996. See also CU/DCS TR 95-04, which can be obtained from the URL
     `ftp://ftp.cs.concordia.ca/pub/chalin/CU-DCS-TR-95-04.ps.Z'.
[Chen89]
     Jolly Chen. The Larch/Generic Interface Language. Bachelor's thesis,
     Massachusetts Institute of Technology, EECS department, May, 1989.
     (Available from John Guttag: [e-mail].)
[Cheon-Leavens94]
     Yoonsik Cheon and Gary T. Leavens. The Larch/Smalltalk Interface
     Specification Language ACM Transactions on Software Engineering and
     Methodology, 3(3):221-253 (July 1994).
[Cheon-Leavens94b]
     Yoonsik Cheon and Gary T. Leavens. A Gentle Introduction to
     Larch/Smalltalk Specification Browsers. Department of Computer Science,
     Iowa State University, TR #94-01, January 1994. Available from the URL
     `ftp://ftp.cs.iastate.edu/pub/techreports/TR94-01/TR.ps.Z'.
[DeMillo-Lipton79]
     Richard A. De Millo and Richard J. Lipton and Alan J. Perlis. Social
     Processes and Proofs of Theorems and Programs. Communications of the
     ACM, 22(5):271-280 (May 1979).
[Edwards-etal94]
     Stephen H. Edwards, Wayne D. Heym, Timothy J. Long, Murali Sitaraman,
     and Bruce W. Weide. Part II: Specifying Components in RESOLVE. ACM
     SIGSOFT Software Engineering Notes, 19(4):29-39 (Oct. 1994).
[Ehrig-Mahr85]
     Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification
     1: Equations and Initial Semantics. EATCS Monographs on Theoretical
     Computer Science, volume 6 (Springer-Verlag, NY, 1985).
[Evans96b]
     David Evans. LCLint User's Guide, Version 2.1, April 1996. Available at
     the following URL
     `http://larch-www.lcs.mit.edu:8001/larch/lclint/guide/'.
[Feijs-Jonkers92]
     L. M. G. Feijs and H. B. M. Jonkers. Formal Specification and Design.
     Volume 35 of Cambridge Tracts in Theoretical Computer Science
     (Cambridge University Press, Cambridge, UK, 1992).
[Fetzer88]
     James H. Fetzer. Program Verification: The Very Idea. Communications of
     the ACM, 31(9):1048-1063 (Sept. 1988).
[Finney96]
     Kate Finney. Mathematical Notation in Formal Specifications: Too
     Difficult for the Masses? IEEE Transactions on Software Engineering,
     22(2):158-159 (February 1996).
[Futatsugi-etal85]
     Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, and Jose
     Meseguer. Principles of OBJ2. In Conference Record of the Twelfth
     Annual ACM Symposium on Principles of Programming Languages, pages
     52-66 (ACM, January 1985).
[Garland-Guttag91]
     S. J. Garland and J. V. Guttag. A Guide to LP, The Larch Prover.
     Technical Report 82, Digital Equipment Corp, Systems Research Center,
     130 Lytton Avenue Palo Alto, CA 94301, December, 1991. This is
     superseded by [Garland-Guttag95].
[Garland-Guttag-Horning90]
     Stephen J. Garland, John V. Guttag, and James J. Horning. Debugging
     Larch Shared Language Specifications. IEEE Transactions on Software
     Engineering, 16(6):1044-1057 (Sept. 1990). Superseded by Chapter 7 in
     [Guttag-Horning93].
[Garland-Guttag95]
     Stephen J. Garland and John V. Guttag. LP, the Larch Prover. On-line
     documentation for release 3.1a (MIT Laboratory for Computer Science,
     April 1995). Available in the LP distribution and from the URL
     `http://larch-www.lcs.mit.edu:8001/larch/LP/contents.html'.
[Goguen-etal87]
     J. Goguen, C. Kirchner, A. Megrelis, J. Meseguer, and T. Winkler. An
     Introduction to OBJ3. In S. Kaplan and J.-P. Jouannaud (eds.),
     Conditional Term Rewriting Systems, 1st International Workshop, Orsay,
     France, pages 258-263. Lecture Notes in Computer Science, Volume 308
     (Springer-Verlag, NY, 1987).
[Goguen-Thatcher-Wagner78]
     J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An Initial Algebra
     Approach to the Specification, Correctness and Implementation of
     Abstract Data Types. In Raymond T. Yeh (ed.), Current Trends in
     Programming Methodology, volume 4, pages 80-149 (Prentice-Hall,
     Englewood Cliffs, N.J., 1978).
[Goguen84]
     J. A. Goguen. Parameterized Programming. IEEE Transactions on Software
     Engineering, SE-10(5):528-543 (Sept. 1984).
[Goguen86]
     J. A. Goguen. Reusing and Interconnecting Software Components IEEE
     Computer, 19(2):16-28 (February 1986).
[Gordon-Melham93]
     M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem
     Proving Environment for Higher Order Logic. Cambridge University Press,
     1993.
[Gries-Schneider95]
     David Gries and Fred B. Schneider. Avoiding the Undefined by
     Underspecification. In Jan van Leeuwen (ed.), Computer Science Today:
     Recent Trends and Developments, pages 366-373. Volume 1000 of Lecture
     Notes in Computer Science (Springer-Verlag, NY, 1995).
[Guaspari-Marceau-Polak90]
     David Guaspari, Carla Marceau, and Wolfgang Polak. Formal Verification
     of Ada Programs. IEEE Transactions on Software Engineering,
     16(9):1058-1075 (Sept. 1990). Reprinted in [Martin-Wing93], pages
     104-141.
[Guttag-Horning-Modet90]
     John V. Guttag, J. J. Horning, and Andres Modet. Report on the Larch
     Shared Language: Version 2.3. Technical Report 58, Digital Equipment
     Corp, Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301,
     April, 1990. Order from [e-mail] or from the URL
     `http://www.research.digital.com/SRC/publications/src-rr.html'.
[Guttag-Horning-Wing85a]
     J. V. Guttag, J. J. Horning, and J. M. Wing. Larch in Five Easy Pieces.
     Technical Report 5, Digital Equipment Corp, Systems Research Center,
     130 Lytton Avenue Palo Alto, CA 94301, July 1985. Superseded by
     [Guttag-Horning93].
[Guttag-Horning-Wing85b]
     John V. Guttag, James J. Horning and Jeannette M. Wing. The Larch
     Family of Specification Languages. IEEE Software, 2(5):24-36 (Sept.
     1985).
[Guttag-Horning78]
     J. V. Guttag and J. J. Horning. The Algebraic Specification of Abstract
     Data Types. Acta Informatica, 10(1):27-52 (1978).
[Guttag-Horning91b]
     J. V. Guttag and J. J. Horning. A Tutorial on Larch and LCL, a Larch/C
     Interface Language. In S. Prehn and W. J. Toetenel (eds.), VDM '91
     Formal Software Development Methods 4th International Symposium of VDM
     Europe Noordwijkerhout, The Netherlands, Volume 2: Tutorials. Lecture
     Notes in Computer Science, vol. 552, (Springer-Verlag, NY, 1991), pages
     1-78.
[Guttag-Horning93]
     John V. Guttag and James J. Horning with S.J. Garland, K.D. Jones, A.
     Modet and J.M. Wing. Larch: Languages and Tools for Formal
     Specification. Texts and Monographs in Computer Science series
     (Springer-Verlag, NY, 1993). (The ISBN numbers are 0-387-94006-5 and
     3-540-94006-5.)
[Guttag75]
     John V. Guttag. The Specification and Application to Programming of
     Abstract Data Types. Ph.D. Thesis, University of Toronto, Toronto,
     Canada, September, 1975.
[Hall90]
     Anthony Hall. Seven Myths of Formal Methods. IEEE Software, 7(5):11-19
     (Sept. 1990).
[Hayes93]
     I. Hayes (ed.), Specification Case Studies, second edition
     (Prentice-Hall, Englewood Cliffs, N.J., 1990).
[Hoare69]
     C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Comm. ACM,
     12(10):576-583 (Oct. 1969).
[Hoare72a]
     C. A. R. Hoare. Proof of correctness of data representations. Acta
     Informatica, 1(4):271-281 (1972).
[Jackson95]
     Daniel Jackson. Structuring Z Specifications with Views. ACM
     Transactions on Software Engineering and Methodology, 4(4):365-389
     (Oct, 1995).
[Jones90]
     Cliff B. Jones, Systematic software development using VDM, second
     edition (Prentice-Hall, Englewood Cliffs, N.J., 1990).
[Jones91]
     Kevin D. Jones. LM3: A Larch Interface Language for Modula-3: A
     Definition and Introduction: Version 1.0. Technical Report 72, Digital
     Equipment Corp, Systems Research Center, 130 Lytton Avenue Palo Alto,
     CA 94301, June, 1991. Order from [e-mail] or from the URL
     `http://www.research.digital.com/SRC/publications/src-rr.html'.
[Jones93]
     Kevin D. Jones. A Semantics for a Larch/Modula-3 Interface Language. In
     [Martin-Wing93], pages 142-158.
[Jonkers91]
     H. B. M. Jonkers. Upgrading the pre- and postcondition technique. In S.
     Prehn and W. J. Toetenel (eds.), VDM '91 Formal Software Development
     Methods 4th International Symposium of VDM Europe Noordwijkerhout, The
     Netherlands, Volume 1: Conference Contributions, volume 551 of Lecture
     Notes in Computer Science, pages 428-456. Springer-Verlag, NY, 1991.
[Khosla-Maibaum87]
     S. Khosla and T. S. E. Maibaum. The Prescription and Description of
     State Based Systems. In B. Banieqbal, H. Barringer, and A. Puneli
     (eds.), Temporal Logic in Specification. Volume 398 of Lecture Notes in
     Computer Science, pages 243-294. Springer-Verlag, NY, 1987.
[Lamport89]
     Leslie Lamport. A Simple Approach to Specifying Concurrent Systems.
     CACM, 32(1):32-45 (Jan. 1989).
[Leavens97]
     Gary T. Leavens. Larch/C++ Reference Manual. Version 5.10, August 1997.
     Available in `ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz' or on
     the world wide web via the URL
     `http://www.cs.iastate.edu/~leavens/larchc++.html'.
[Leavens96b]
     Gary T. Leavens. An Overview of Larch/C++: Behavioral Specifications
     for C++ Modules. Technical Report TR #96-01d, Department of Computer
     Science, Iowa State University, Ames, Iowa, 50011, April 1996, revised
     July 1997. In Haim Kilov and William Harvey, editors, Specification of
     Behavioral Semantics in Object-Oriented Information Modeling (Kluwer
     Academic Publishers, 1996), Chapter 8, pages 121-142. TR version
     available from the URL
     `ftp://ftp.cs.iastate.edu/pub/techreports/TR96-01/TR.ps.gz'.
[Leavens-Wing97]
     Gary T. Leavens and Jeannette M. Wing. Protective Interface
     Specifications In Michel Bidoit and Max Dauchet (editors), TAPSOFT '97:
     Theory and Practice of Software Development, 7th International Joint
     Conference CAAP/FASE, Lille, France, pages 520-534. An extended version
     is Technical Report TR #96-04c, Department of Computer Science, Iowa
     State University, Ames, Iowa, 50011, April 1996, revised October,
     December 1996, February 1997. Available from the URL
     `ftp://ftp.cs.iastate.edu/pub/techreports/TR96-04/TR.ps.gz'.
[Lerner91]
     Richard Allen Lerner. Specifying Objects of Concurrent Systems. School
     of Computer Science, Carnegie Mellon University, CMU-CS-91-131, May
     1991. Available from the URL
     `ftp://ftp.cs.cmu.edu/afs/cs.cmu.edu/project/larch/ftp/thesis.ps.Z'.
[Liskov-Guttag86]
     Barbara Liskov and John Guttag. Abstraction and Specification in
     Program Development (MIT Press, Cambridge, Mass., 1986).
[Loeckx-Ehrich-Wolf96]
     Jacques Loeckx, Hans-Dieter Ehrich, and Markus Wolf Specification of
     Abstract Data Types (John Wiley & Sons Ltd and B. G. Teubner, NY,
     1996).
[Luchangco-etal94]
     Victor Luchangco, Ekrem Soylemez, Stephen Garland, and Nancy Lynch.
     Verifying timing properties of concurrent algorithms. In FORTE'94:
     Seventh International Conference on Formal Description Techniques for
     Distributed Systems and Communications Protocols, Berne, Switzerland
     (Chapman and Hall, Oct. 1994).
[Martin-Lai92]
     U. Martin and M. Lai. Some experiments with a completion theorem
     prover. Journal of Symbolic Computation, 13:81-100 (1992).
[Martin-Wing93]
     U. Martin and J. Wing. Proceedings of the First International Workshop
     on Larch, July 1992. Workshops in Computing series (Springer-Verlag,
     New York, 1993). (The ISBN is 0-387-19804-0.)
[Meyer92]
     Bertrand Meyer. Applying "Design by Contract". Computer, 25(10):40-51
     (Oct. 1992).
[Meyer97]
     Bertrand Meyer. Object-oriented Software Construction, second edition
     (Prentice-Hall, 1997).
[Mosses96]
     Peter D. Mosses (editor). CFI Catalogue: Language Design. May 1996.
     Available from the URL
     `http://www.brics.dk/Projects/CFI/Catalogue/2/index.html'.
[ORA94]
     Odyssey Research Associates. Penelope Reference Manual, Version 3-3.
     Informal Technical Report STARS-AC-C001/001/00, September 1994.
     Available from the URL
     `http://source.asset.com/WSRD/ASSET/A/874/elements/RefManual.tty'.
[Owre-etal95]
     Formal Verification for Fault-tolerant Architectures: Prolegomena to
     the Deisgn of PVS. Sam Owre, John Rushby, Natarajan Shankar, and
     Friedrich von Henke. IEEE Transactions on Software Engineering,
     21(2):107-125 (February 1995).
[Saiedian-etal96]
     An Invitation to Formal Methods. Hossein Saiedian, et al. IEEE
     Computer, 29(4):16-30 (April 1996).
[Saxe-etal92]
     J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning. Using
     transformations and verification in circuit design. International
     Workshop on Designing Correct Circuits, IFIP Transactions A-5,
     (North-Holland 1992). Also Technical Report 78, Digital Equipment Corp,
     Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301,
     September 1991.
[Schmidt86]
     David A. Schmidt. Denotational Semantics: A Methodology for Language
     Development (Allyn and Bacon, Inc., Boston, Mass., 1986).
[Sitaraman-Welch-Harms93]
     M. Sitaraman, L. R. Welch, and D. E. Harms. On Specification of
     Reusable Software Components. International Journal of Software
     Engineering and Knowledege Engineering, 3(2):207-229 (World Scientific
     Publishing Company, 1993).
[Sivaprasad95]
     Gowri Sankar Sivaprasad. Larch/CORBA: Specifying the Behavior of
     CORBA-IDL Interfaces. Department of Computer Science, Iowa State
     University, TR #95-27a, December 1995, revised December 1995.
[Soegaard-Anderson-etal93]
     J. F. Soegaard-Anderson, S. J. Garland, J. V. Guttag, N. A. Lynch, and
     A. Pogosyants. Computed-assisted simulation proofs. In Fourth
     Conference on Computer-Aided Verification, Elounda, Greece, Volume 697
     of Lecture Notes in Computer Science, pages 305-319 (Springer-Verlag,
     June 1993).
[Spivey92]
     J. Michael Spivey. The Z Notation: A Reference Manual, second edition,
     (Prentice-Hall, Englewood Cliffs, N.J., 1992).
[Staunstrup-Garland-Guttag89]
     J. Staunstrup, S. J. Garland, and J. V. Guttag. Localized verification
     of circuit descriptions. In Proc. Int. Workshop on Automatic
     Verification Methods for Finite State Systems, Grenoble, France. Volume
     407 of Lecture Notes in Computer Science, pages 349-364
     (Springer-Verlag, 1989).
[Staunstrup-Garland-Guttag92]
     J. Staunstrup, S. J. Garland, and J. V. Guttag. Mechanized verification
     of circuit descriptions using the Larch Prover. In Theorem Provers in
     Circuit Design. IFIP Transactions A-10, pages 277-299 (North-Holland,
     June, 1992).
[Tan94]
     Yang Meng Tan. Formal Specification Techniques for Promoting Software
     Modularity, Enhancing Documentation, and Testing Specifications. MIT
     Lab. for Comp. Sci., TR 619, June 1994. Also published as Formal
     Specification Techniques for Engineering Modular C Programs.
     International Series in Software Engineering (Kluwer Academic
     Publishers, Boston, 1995).
[Wing-Rollins-Zaremski93]
     Jeannette M. Wing, Eugene Rollins, and Amy Moormann Zaremski. Thoughts
     on a Larch/ML and a New Application for LP. In [Martin-Wing93], pages
     297-312.
[Wing83]
     Jeannette Marie Wing. A Two-Tiered Approach to Specifying Programs
     Technical Report TR-299, Mass. Institute of Technology, Laboratory for
     Computer Science, 1983.
[Wing87]
     Jeannette M. Wing. Writing Larch Interface Language Specifications. ACM
     Transactions on Programming Languages and Systems, 9(1):1-24 (Jan.
     1987).
[Wing90]
     Jeannette M. Wing. A Specifier's Introduction to Formal Methods.
     Computer, 23(9):8-24 (Sept. 1990)
[Wing95]
     Jeannette M. Wing. Hints to Specifiers. Technical Report,
     CMU-CS-95-118R, Carnegie Mellon University, School of Computer Science,
     May 1995. Revision of the paper, "Teaching Mathematics to Software
     Engineers," Proceedings of AMAST '95, July 1995. Revision available
     from the URL
     `http://www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/papers/education/paper.ps'.


Footnotes

(1)

Although one cannot list both unknown and hmm in the same converts clause,
one could add another converts clause to the trait ConvertsTrait, stating
that unknown is converted, relative to the other operators, which in that
case include hmm.

(2)

The semantics of a Larch BISL is not fixed by being a member of the family,
but there is a family resemblance, due mostly to the common heritage from
Larch/CLU [Wing83]. The remarks about BISLs should be taken as generalities
about the family, especially about BISLs for sequential programming
languages like C and C++, and might not hold for your particular BISL.
Consult the documentation for your particular BISL to be sure.

------------------------------------------------------------------------

This document was generated on 20 October 1997 using the texi2html
translator version 1.50.
--
        229 Atanasoff Hall, Department of Computer Science
        Iowa State Univ., Ames, Iowa 50011-1040 USA
        [e-mail]  phone: [phone] fax: [phone]
        URL: http://www.cs.iastate.edu/~leavens/homepage.html