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

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 ...
  ------------------------------------------------------
  ~(E1 = E2)            resume by contradiction
                          % sometimes followed by
                          critical-pairs *Hyp with *
  P1 /\ P2 /\ ...       resume by /\
  P => Q                resume by =>
  P <=> Q               resume by <=>
  if H then P else Q    resume by if-method
  ...(if P then ...)... resume by cases P
  \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.

For complex proofs, it is quite useful to prove lemmas first. You can either
state these as things to be proved before what you are trying to prove, or
use the prove command during the proof. You may need to use the command set
immunity on to keep LP from deleting your lemma after you prove it.

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: put the command set box-checking on at the top of your proof,
     so that these box comments will be checked. You only need this once per
     file.
  7. 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.
  8. 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

  9. 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'.
 10. 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.

        20a21
        > set box-checking on
        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] [Evans00]) 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 URL.

       http://lclint.cs.virginia.edu/

     There is also a mailing list for LCLint, which you can subscribe to
     using the first URL above, or by sending email to
     lclint-request@virginia.edu.
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 marketing@oracorp.com). Information on Penelope and AdaWise is
     available at the following URLs.

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

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

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

© allanswers.org | Terms of use