[Prev][Next][Index]

Patrice Chalin's "Shortcomings of LCL 2.4"

I commend to your attention Patrice Chalin's report "Shortcomings of LCL 2.4"
(Concordia University TR CU/DCS-TR-95-04, April 1995).
The TR can be obtained by anonymous ftp at ftp.cs.concordia.ca in
pub/chalin/CU-DCS-TR-95-04.ps.Z.

I have read this report several times, and it's of great interest
to designers of interrface specification languages, and those interested
in their semantics.  It is of particular interest to me, because the
design of Larch/C++ is based on LCL.

The following briefly summarizes the points I thought were most interesting
(probably because they bear on Larch/C++).

1. LCL has no way to specify aliasing; Chalin recommends that new primitives
   be added that allow "dependency" relationships to be expressed. (Section 2.)

   In Larch/C++, I believe that one can express such relationships using
   reified states, although I haven't tried to do so yet in detail.)

2. LCL has no way to specify that a pointer is non-null, and points
   to properly allocated storage.  It has no way to say that such storage
   must be initialized.  The same holds for array parameters.  (Section 3.)

   This seems to be due to the high-level view taken of pointers and arrays
   in LCL.  In Larch/C++, one can express that a pointer must be valid,
   this is because the model of pointers is more detailed than in LCL.
   Alas, in Larch/C++, there is no way to say that an array parameter has
   to be non-null, etc.  I am afraid I'll have to change Larch/C++ to make
   array parameters be the same as pointers (as in C++ itself).

   I don't see why one needs to worry about storage being initialized.
   It seems impossible to test this, and real storage always has some
   values in it.  Can someone explain this concern further?  Is it orthogonal
   to other aspects of verification?

3. Something about the semantics of "trashed" is clearly wrong in LCL.
   It's either the remark that
	 modifies *i
   does not include the possibility that *i may be deallocated,
   or the ability to say things like
	ensures trashed(*i) \/ ~trashed(*i)

   In looking at the formal model of states for Larch/C++, I think the
   explanation is that the remark that
	modifies *i
   does not include the possibility that *i may be deallocated is wrong.
   Deallocation is a subset of modification, and I think this solves this
   problem neatly enough, although it may be tricky to keep in mind.

Chalin also points out other interesting issues, like trashing parts
of objects.  In section 5.2, it seems that the problem pointed out is
that an aarray name is treated as an object, whereas it is not one.

I welcome further discussion of this.

	Gary
--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html