[PRL] Contracts vs aspects

[Pengcheng Wu]

On Thu, 28 Apr 2005, Mitchell Wand wrote:

> Adrian Collyer writes (at
> http://www.aspectprogrammer.org/blogs/adrian/2005/04/aspects_as_auto.html):
>
>  We'll need a requirement to work from. Let's take good old
>  foobar. Everyone knows that foo comes before bar. What if we wanted
>  to write an aspect to make sure that was true? More precisely, let's
>  write an aspect to enforce the following rule:
>
>     Every call to bar() within an action must be preceded by at least
>     one call to foo(). After any call to bar(), foo() must be called
>     at least once before bar() can be called again.

Seems to me that Collyer's solution is much less elegant than the trace
matching solution by Oege de Moor et al, which is very declarative and
doesn't put the burden of state maintenance on the programmers' side.

They have a tech. report at:

 http://abc.comlab.ox.ac.uk/documents/abc-2005-1.pdf

Using their approach, I could come up with an aspect checker of the above
rules as easy as the following (I didn't actually run it):

tracematch() {
  sym notfoocall after: call(!foo(..));
  sym foocall after: call(foo(..));
  sym barcall before: call(bar(..));
  sym barcallafter after: call(bar(..));

  notfoocall* barcall {
     error("bar without foo");//rule 1 violation
  }

  barcallafter notfoocall* barcall {
     error("bar calls without foo in the middle");//rule 2 violation
  }
}

Their compiler will generate the corresponding state transition code.

--Pengcheng