[Prev][Next][Index]

``imports'' clause


Hi,

my name is Wilma Penzo and I am a Ph.D. student at the
University of Bologna. My topics of interest deal with
formal methods in software engineering and I am very
interested in the use of Larch as a specification language.

The following messages have been already sent to the 
lclint-interest mailing-list, but I think the contents
could be of general interest, so I place them here too.
I would like to know what do you think about it.

---- first message ------

At present I am involved in the specification of a simple
case study and the use of the LCLint tool is giving me
some problems.

In particular, I'd have a question about the use of the 
``imports'' clause in the description of LCL modules.
With reference to the book ``Larch: languages and tools for
formal specification'' - Guttag - Horning, ``imports'' is
used with the aim of allowing the access to constants, types
and functions previously defined in the ``imported'' module.
Unfortunately no explicit example is made about a possible
reuse of functions and I can not understand why LCLint
does not pass the check for modules like the following 
(which are simplified so as to be clearer):

# BirthdayBook.lcl
^^^^^^^^^^^^^^^^^^

immutable type NAME;
immutable type DATE;

mutable type BDB;

uses BirthdayBook;

void Addbirthday(BDB bdb, NAME n, DATE d) {
  modifies bdb;
  ensures bdb'.k = addName(n, bdb^.k) /\
          bdb'.b = addBirthday(bdb^.b, n , d);
}


# Error_Messages.lcl
^^^^^^^^^^^^^^^^^^^^

immutable type REP;

uses RepBirth;

REP Success() {
  ensures result = Okay;
}

REP AlreadyKnown() {
  ensures result = Already_Known;
}


# Complete_BDB.lcl
^^^^^^^^^^^^^^^^^^^^^^^^^^^

imports BirthdayBook;
imports Error_Messages;

REP RAddbirthday(BDB bdb, NAME n, DATE d) {

  modifies bdb;
  ensures if \not(n \in bdb^.k) then (Addbirthday(bdb, n, d) /\
                                     result = Success)
                                else result = AlreadyKnown;
}


The corresponding LCLint output message is:
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

LCLint 1.4 --- Thu Sep 29 14:37:28 EDT 1994

Complete_BDB.lcl:8,47: Unrecognized identifier (constant, variable or operator):
                          Success
Complete_BDB.lcl:9,47: Unrecognized identifier (constant, variable or operator):
                          AlreadyKnown
Complete_BDB.lcl:7,39: Undeclared operator: Addbirthday
Finished LCLint checking --- 3 spec errors found / no code processed



It seems as if the specified operators have not been exported in the
right way. Nevertheless, the .lcs and .lh files have been produced.

Does anyone know why the tool behaves in this way? 
Where could have been possible mistakes? 
Is there a special option to be considered while the lclint program
is called?


Thanks in advance.

Wilma


--------- second message -----

> It seems as if the specified operators have not been exported in the
> right way. Nevertheless, the .lcs and .lh files have been produced.

The problem here is some confusion between LCL functions and LSL
operators.  In the ensures clause, only LSL operators may be used.  So
the specification for RAddbirthday should use the LSL operators Okay and
Already_Known instead of Success and AlreadyKnown (which I presume were
only defined as LCL functions).  You would also need to add an LSL
operator comparable for Addbirthday and replace this in the
specification.

--- Dave


------- third message --------------------

> 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