[Prev][Next][Index]

Re: specification of destructive operation (correction to Larch/C++ spec)

Arnd,

I made a mistake in the example I sent.  The following explains the details.
(Or maybe the date explains the details; hmm... :-)

   Date: Fri, 13 Jan 95 14:09:21 CST
   From: leavens (Gary Leavens)

   P.S. I had to make a couple of fixes in Larch/C++ to parse this (:-)
   and I had to update a trait to specify this easily; so if you get Larch/C++
   or the manual close to the time this is sent, it may not work on this spec.
   But it will, and that's a benefit of doing such an exercise.

I was a bit too hasty in allowing the use of reach within fresh,
which showed up in the following.

   list  copy( list l ) {
     uses ToListTrait;
     requires isLegal(l);
     ensures fresh(reach(result))
             /\ toList(l,pre) = toList(result,post);
   }

This seemed like a good idea at the time, but the semantics of reach
uses the pre-state, while fresh necessarily uses the post-state,
and so the above is a mess.  The correct way to do this involves
writing more trait functions, and using those within fresh.
In this case the trait function is list_objs, which takes the appropriate
state as an argument.  This also shows the key idea: the interface
language has to be the source of the state passed to the trait functions.
This is why pre and post (and any) are reserved words in Larch/C++.

list  copy( list l ) {
  uses ToListTrait;
  requires isLegal(l) /\ not(circular(l));
  ensures fresh(list_objs(result, post))
          /\ toList(l,pre) = toList(result,post);
}

The trait function list_objs fits in with the ToListTrait.

ToListTrait: trait
  % ... as before ...
  introduces
    list_objs: Ptr[Obj[listelem]], St -> Set[Object]
  asserts \forall p: Ptr[Obj[listelem]], st: St
    list_objs(NULL, st) == {};
    (isValid(p) /\ not(circular(p, st)))
	=> (list_objs(p, st) = {widen(*p)} \U list_objs(((*p)!st).cdr, st))

Sorry for any confusion this mistake may have caused.

	Gary

	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/larchc++.html
Reference(s):