[Prev][Next][Index]
Re: specification of destructive operation
Arnd,
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".
Gary
Follow-Up(s):
Reference(s):