[Prev][Next][Index]

Re: Basic LSL Questions

schroed@schubert.cs.colostate.edu ( stephen schroeder) wrote:
>
>I have a couple simple questions regarding LSL traits.
>
>1-I'm assuming that a trait definition with an includes statement
>can be replaced with the trait definitions and all definitions in
>the included trait.  

This is correct.

>I don't quite understand what 'discharging' the
>definitions mean for an assumes statement.  Does it simply mean
>to ignore the definitions for any trait if it is included or assumed
>by a 'parent' trait?
>
>	eg	X:trait
>			Includes Y,Z
>		
>		Y:trait
>			Includes A
>			Assumes B
>
>	Does this mean that X would inherit all of A's
>	definitions and ignore B's definitions?  How would
>	conflicting definitions be handled.

Assumptions are requirements that the specifier imposes on the contexts in
which traits are used.  In this example, the assumes clause in Y means that B
must be provable in any context in which Y is used (i.e., included or assumed).
If the definitions of the traits X and Y shown here are complete, the assumes
clause means that B must be provable from Z to satisfy the requirement it
imposes on the context in which Y is used.

>2-Are implies statements used only in proofs about the trait,
>or are traits given on an implies statement also inherited by
>the parent trait?

Putting aside for the moment the question of checking implies clauses, the
traits listed in them are indeed inherited by parent traits.  The "theory" of a
trait is the set of all statements that follow from the axioms of the trait.
An implies clause claims (or calls attention to the fact) that certain
statements are in the theory of the trait.  When a trait is included or assumed
by another, its theory is a subset of the theory of the parent trait.

When it comes to verifying the claims made in an implies clause, one has to be
careful not to use circular reasoning.  Hence, when checking the implications
of some trait, it is safe to use the implications of a subtrait only if those
implications have already been checked.
Reference(s):