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

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 generated freely by clause
in the most recent versions of LSL. The use of a generated freely 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

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

© allanswers.org | Terms of use