[Prev][Next][Index]

Re: assumes and includes

Paolo,

This is one of the most difficult features of LSL to explain, although
we've tried hard in the papers and the book.  Let me try once more:

Think of assumes clauses as restrictions on the environment and formal
parameters of a trait, much like types on the formal parameters of a
procedure.  This means that within the trait, you can use the assumed
operators freely without defining them, knowing that they will be supplied
by "the environment."  For this to be sound, there needs to be a check on
each instantiation of the trait to ensure that those operators are indeed
available and do have the assumed properties.  (This is somewhat analogous
to checking that actual parameters of a procedure have the types declared
for the formals.)

Includes clauses, on the other hand, directly incorporate the referenced
traits.  They do not impose proof obligations at the point of
instantiation, because the referenced traits are also instantiated.

When writing traits, it is fine to begin by using only includes clauses.
But after you have built the theory you want, and are fine-tuning the
structure, you may want to change some includes clauses to assumes clauses:

- To document that the theory is supposed to come from the environment.
E.g., PriorityQueue assumes TotalOrder(E for T).  This means that there
must be a total order on the element sort of the queue, but the particular
order is not specified by PriorityQueue itself.

- To document that a trait only makes sense in a certain context.
E.g., ReverseOp assumes List.  It defines reverse in terms of several list
operators, and isn't really useful if those operators aren't available.

- To get additional checking that the definitions mentioned above haven't
been omitted.

- To make it possible to prove implications that depend on the assumed
theories.

Hope this helps,

Jim H.