[Prev][Next][Index]

Re: specification of destructive operation


Gary,
        obviously I didn't succeed in posing my questions clear 
enough. Let me try to rephrase it. Below you find a rather
ordinary  C module implementing linked int lists. The client of 
such a module should be allowed to assign lists to variables;
i.e. s/he has the responsibility of keeping track of sharing.
I am looking for a way to specify such modules. In particular,
the specification should tell the client which procedures
 -  introduce sharing  (e.g. append introduces sharing between 
       its second argument and its result)
 -  destroy list representations (e.g. conc destroys the representation
       of its first argument (and introduces sharing of the result and
       the second argument)
 -  provide fresh representations (e.g. copy)
Given such specifications the client should be able to handle
sharing in a safe and effective way.

As far as I understand LCL, I can not specify such modules as
abstract types. On the other hand, I like to use a list
trait to specify the functional behaviour of the procedures.

So, let me pose my questions again:

- How can such implementations be specified in LCL or LM3, if it is
  possible at all?

- Are there other LARCH interface languages that support the specification
  of such modules ?

Further comments are very wellcome.

Thanks in advance,

      Arnd.


==============================================================

typedef struct  listelem {
	int    head;
        struct listelem* tail;} * list;        

list  empty()			{  return NULL; }
bool  isempty( list l )		{ ... }
bool  equal( list l1, list l2 )	{ ... }
int   top( list l )		{  return l->head;  }
list  rest( list l )		{  return l->tail;  }
list  append( int i, list l )	{ 
... }
list  copy( list l )		{ ... }
list  conc( list l1, list l2 ){ 
	list lvar = l1 ;
	if( isempty(lvar) ){
	   return  l2;
        } else {
	   while(  ! isempty( rest(lvar) )  )  lvar = rest(lvar);
	   lvar->tail = l2;
	   return  l1;
	}
    }
Follow-Up(s): Reference(s):