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

above list. (Of course, you'd never write anything this bad.)

NonAbstractSet: trait
  includes Integer

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.23 Where can I find handbooks of LSL traits?

The most commonly-used handbook of LSL traits is Guttag and Horning's
handbook ([Guttag-Horning93], Appendix A). This can be obtained by anonymous
ftp with the LSL checker (see section 2.3 Where can I get a checker for
LSL?). A hypertext version is on-line in

  http://www.research.digital.com/SRC/larch/toc.html

A general resource for all known handbooks that are publically available is
found on the world-wide web, at the following URL.

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

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

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

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

In LSL 3.1, you can write a universal quantifier within an LSL term by using
\A, and an existential quantifier using \E. As an example, consider the
following trait (from Leavens's Math handbook).

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

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

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

You can get a LaTeX style file, `larch.sty', and a macro file defining a
bunch of mathematical symbols, `larchmath.tex', by anonymous ftp from the
following URL.

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

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

The documentation for `larch.sty' says that it is to be used with LaTeX
2.09. However, it can be used with LaTeX2e. To do so, put the following
lines at the start of your LaTeX input.

\documentclass{article}
\usepackage{larch}

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

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

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

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

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

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

Yes, there actually is a version of "spiderweb" specialized for use with
LSL. If you are really a fan of such fancy systems, you can find it by using
the literate programming library's URL.

  http://www.desy.de/user/projects/LitProg.html

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

However, we have found that using the "noweb" system is much easier for most
people, and nearly as good. You can get noweb from the literate programming
library (see above), or directly from the following URL.

  http://www.eecs.harvard.edu/~nr/noweb/intro.html

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

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

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

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

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

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

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

  lcpp2html -P -I *.lsl

3. The Larch Prover (LP)

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

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

3.1 What is the Larch Prover (LP)?

The Larch Prover (LP) [Garland-Guttag95] is a program that helps check and
debug proofs. It is not geared toward proving conjectures automatically, but
rather toward automating the tedious parts of proofs. It automates
equational rewriting (proofs by normalization), but does not (by default)
automatically try other proof techniques.

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

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

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

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

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

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

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

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

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

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

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

3.3 How does LP compare with other theorem provers?

The basic difference between LP and other theorem provers is that LP does
not automatically attempt complex (i.e., interesting or speculative) proof
steps. LP also has no way to write general proof strategies or tactics (as
can be done in PVS, LCF, and other theorem provers). An additional
convenience is that there are tools for supporting the translation of LSL
specifications into LP's input format.

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

The Boyer-Moore theorem prover, NQTHM [Boyer-Moore79] [Boyer-Moore88] is
also more agressive than LP in trying to actively search for proofs. Its
successor, ACL2 is described as "industrial strength" [Kaufmann-Moore97].

A major difference between LP and HOL [Gordon-Melham93], Isabelle
[Paulson94], and PVS is that LP does not use a higher-order logic, which the
others do. Isabelle also has extensive support for term rewriting.

[[[Should also compare to OTTER, and RRL. Contributions are welcome
here...]]]

3.4 Where can I get an implementation of LP?

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

  http://www.sds.lcs.mit.edu/spd/larch/LP/news/distribution.html

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

  ftp://ftp.sds.lcs.mit.edu/pub/Larch/LP/

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

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

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

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

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

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

3.6 Can I change the erase character in LP?

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

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

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

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

3.7 How do I interrupt LP?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

       lsl -lp Foo.lsl

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

       lp

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

       execute Foo_Checks

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

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

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

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

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

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

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

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

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

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

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

  All conjectures have been proved.

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

  Still attempting to prove level 2 lemma FooTheorem.2

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

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

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

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

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

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

© allanswers.org | Terms of use