``imports'' clause

To: wilma@deis65.cineca.it
Subject: ``imports'' clause
From: evs@sds.lcs.mit.edu (David Evans)
Date: Mon, 7 Nov 94 15:40:09 -0500
Cc: lclint-interest@larch.lcs.mit.edu
Delivery-Date: Mon, 07 Nov 94 12:56:27 -0800
In-Reply-To: Wilma Penzo's message of Mon, 7 Nov 1994 21:18:02 +0100 (MET) <9411072018.AA05712@deis65.cineca.it>


Sorry, my earlier answer was somewhat unclear.  LCL types, variables and
constants may be used, but not functions.  (My guess is that this was
done to make the distinction between the interface specification and the
shared specification clear and to make sure the ensures clause has
defined semantics?  Perhaps Yang Meng, Jim or John can clarify/correct
me on this one.)

Note that this doesn't have anything to do with the imports clause.  You
cannot use an LCL function in the ensures clause even if it is defined
in the same LCL module.  

> Well, there was any confusion in the use of LCL functions in
> the ensures clause. I purposely used them since I believed 
> it was possible (as it is suggested in the literature).

Where?  It shouldn't be.  (Although, the only clear explanation I could
find of what goes in a function specification is in Yang Meng Tan's
thesis (MIT/LCS/TR-619) p. 109.)

Hope this clears things up,

--- Dave

Reference(s):

``imports'' clause

From: wilma@deis65.cineca.it (Wilma Penzo)