[Prev][Next][Index]
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.
--
=================================================================
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
Germany
Follow-Up(s):