specification of destructive operation

Dear Larch people,

I am looking for a way to specify implementation modules of "abstract data
types". Allmost all the modules I looked at make destructive operations
available to the user. Consider e.g. a list implementation that 
provides a concatenation procedure 

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

that destroys the representation of the list l1 and that of all lists 
shared with l1. I would like to specify it as

REQUIRES  legal(l1)  and  legal(l2)  and  not shared(l1,l2)
MODIFIES  l: List. shared(l,l1)
ENSURES   legal(result)  
          and  a_conc( abs(l1)^, abs(l2)^ ) = abs( result )

where "legal" assures that a list variable points to a legal 
list represantion (no cycles, ...), "a_conc" denotes the
abstract list concatenation and "abs" is an abstraction function
mapping legal list representation to abstract lists.
"legal", "shared", and "abs" are provided by the implementor of
the list module.

My questions:

- As far as I understood, such a specification style is not supported
  by LCL or LM3; or did I miss I something? 

- How can such implementations be specified in LCL or LM3?

- Is such a style supported by other LARCH interface languages?

Further comments are very wellcome.

Thanks in advance,



 Arnd Poetzsch-Heffter           phone:  ++49 89 2105 8188
   Fakultaet fuer Informatik     fax  :  ++49 89 2105 8180
   Technische Universitaet       email:  poetzsch@informatik.
   D-80290 Muenchen                              tu-muenchen.de