Patrice Chalin's "Shortcomings of LCL 2.4"
Subject: Patrice Chalin's "Shortcomings of LCL 2.4"
From: email@example.com (Gary Leavens)
Date: 13 Jun 95 02:47:17 GMT
Keywords: LCL, C, definedness, pointers, trashed
Organization: Iowa State University, Ames, Iowa
Summary: read it if you're interested in interface language design
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
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
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
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.
229 Atanasoff Hall, Department of Computer Science
Iowa State Univ., Ames, Iowa 50011-1040 USA / firstname.lastname@example.org
phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu