allanswers.org - Larch Frequently Asked Questions (comp.specification.larch FAQ)

 Home >  FAQ on different themes >

Larch Frequently Asked Questions (comp.specification.larch FAQ)

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


Posted-By: auto-faq 3.2.1.4
Archive-name: larch-faq
Posting-Frequency: monthly
Version: 1.116
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

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.116 $

18 July 2001

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?
   * Bibliography
   * Footnotes

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

Introduction

This document is 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
larch-faq@cs-DOT-iastate-DOT-edu (after changing each "-DOT-" to "."). We
will welcome and acknowledge any help you may give.

Bibliographic references are described at the end of this document (see
section 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.

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, Pieter Bekaert, Eric Eide, John
Fitzgerald, Jim Horning, Ursula Martin, Bertrand Meyer, Clyde Ruby, and
Jeannette Wing for general comments, updates, and corrections to this FAQ.
Thanks to Steve Garland and Jim Horning for help with answers. Thanks to
Pierre Lescanne, Kishore Dhara, Teo Rus, Narayanan Sridhar, and
Sathiyanarayanan Vijayaraghavan 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] [Evans00], 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] [ISO-VDM96] [Fitzgerald-Larsen98] 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] [ISO-VDM96]
     [Fitzgerald-Larsen98], then one cannot specify all interface details.
   * The division into two tiers allows the language used for each tier to
     be more carefully designed and expressive. 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] [ISO-VDM96]
[Fitzgerald-Larsen98], Z [Hayes93] [Spivey92], and COLD-K [Feijs-Jonkers92]
are all integrated languages, which mix aspects of both of the tiers of the
Larch family. 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]
[ISO-VDM96] [Fitzgerald-Larsen98]. In comparison with LSL, in VDM-SL one can
specify mathematical values (models) using constructs similar to those in
denotational semantics and typed, functional programming languages. 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

The above example uses the interchange syntax of VDM-SL [ISO-VDM96] is used.
In this syntax, for example, * is an approximation to the mathematical
notation for a cross product; see Section 10 of [ISO-VDM96] for details. 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

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

Back to category FAQ on different themes - Use Smart Search
Home - Smart Search - About the project - Feedback

© allanswers.org | Terms of use

LiveInternet