Re: specification of destructive operation

	I think you misunderstand the semantics of formal parameter
names in LCL, LM3, and perhaps other Larch interface specification languages.
In these languages, the denotation of a parameter such as l1 or l2 in

PROC conc( l1:List, l2:List ):  List

would be the object denoted by these formals in the pre-state.
Hence, one can write a trait function "shared" that takes two objects
and compares them easily:

	shared(l1,l2) == (l1 = l2)

Similarly, the modifies clause describes a set of objects,
not a set of variable names, that may be modified.

Typically also one would not need to have a trait function "legal",
as that would be subsumed by the invariant of the ADT List.

The meaning of "result" *is* the abstract value of result,
and thus one never needs to write "abs".


Follow-Up(s): Reference(s):