Re: ``imports'' clause


    So, this means that LCL operators cannot be used in
    other LCL modules? 


    Is there a reason for this?

Yes, there is.  C "functions" are actually procedures, and can have side
effects, encounter runtime errors, etc.  In our predicates, we want true
mathematical functions.  This is one of the principal motivations for
Larch's two-tiered approach.

We expect much of the "structured" modularity to result from LSL traits
using other traits.  Operators defined in this way can be used both to give
almost trivial specification of the LCL operators you wanted to use and to
specify the other LCL modules in which you wanted to use them.

We consider it an advantage that each LCL module can be specified and
studied, (and perhaps verified) separately, just as it is an advantage to
give a specification for each C function that allows it to be specified and
studied, (and perhaps verified) separately.  Do not confuse the "uses"
hierarchy of module implementations with the structure of their

Jim H.