specification of destructive operation

To: poetzsch@informatik.tu-muenchen.de
Subject: specification of destructive operation
From: evs@sds.lcs.mit.edu (David Evans)
Date: Fri, 13 Jan 95 15:21:55 -0500
Cc: larch-interest@src.dec.com
Delivery-Date: Fri, 13 Jan 95 12:38:57 -0800
In-Reply-To: Poetzsch-Heffter's message of Fri, 13 Jan 1995 18:06:44 +0100 <95Jan13.180653mesz.47388@hpeick9.informatik.tu-muenchen.de>


Arnd,

Some of what you suggest is possible in LCL, except there is no way to
express sharing.  In particular,

> -  destroy list representations (e.g. conc destroys the representation
>       of its first argument (and introduces sharing of the result and
>       the second argument)

	Use trashed(l1) --- trashed says that after returning nothing
	can be assumed about l1.
	
> -  provide fresh representations (e.g. copy)

	Use fresh(result) --- fresh means its argument is not aliased to
	any objects in the pre-state.

To express sharing you would need to do something more complicated, as
Gary suggests.

--- Dave

Reference(s):

Re: specification of destructive operation

From: Poetzsch-Heffter <poetzsch@informatik.tu-muenchen.de>

Prev: Re: specification of destructive operation (correction to Larch/C++ spec)
Next: Re: specification of destructive operation
Index: Larch archive index