lclint-interest message 12
From: wilma@deis65.cineca.it (Wilma Penzo)
Subject: ``imports'' clause
To: lclint-interest@larch.lcs.mit.edu
Date: Mon, 7 Nov 1994 21:18:02 +0100 (MET)
X-Mailer: ELM [version 2.4 PL23]
Content-Type: text
Content-Length: 723
> The problem here is some confusion between LCL functions
> and LSL operators. In the ensures clause, only LSL
> operators may be used.
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).
So, this means that LCL operators cannot be used in
other LCL modules?
I think that the ``imports'' clause has been introduced
in order to allow a ``structured'' modularity. If inclusion
between LCL modules is not possible, then the LCL layer
specification is reduced to a flat set of independent
modules. Is there a reason for this?
I will really appreciate any opinion about this.
Bye
Wilma
David
Evans
University of Virginia, Computer Science
evans@cs.virginia.edu