Re: [abc] RE: nice tracematch...

Eric Bodden wrote:
> I have checked in the attached tracematches to
> tmbenches/runtime-verification/reader-writer.
>
> For the "reader" example, we can IMHO unfortunately not cover all error
> cases, as readers can be arbitrarily stacked on top of each other (c.f.
> tainted String example in PQL). Well, for writers, we essentially have
> the same problem, but there I think it is most common to just create a
> simple PrintWriter directly on top of a single stream.
>
> Eric
>
I don't actually agree with your patterns. In the second tracematch, the
pattern you use is

    create (closeR|closeI) (readR|readI)

I don't see why the sequence 'create closeR readI' should throw an
exception (i.e. we create a reader around something, close the reader,
and read from the something -- the same argument applies to the first
tracematch).

Also, I do think that we can capture all violations, no matter how
stacked on top of each other. It does require a bit of fiddling
though.... The approach might be as follows.

- Define a static method invalidate(Object o) in the aspect (empty body).
- Define a tracematch that, whenever it sees the creation of a reader or
writer O on a subject I (either a stream or another reader/writer),
followed by a call to (I.close() | this.invalidate(I)), calls
this.invalidate(o).
- Define a tracematch that, whenever it sees a call to
this.invalidate(o) followed by o.read() or o.write(), throws an exception.

Admittedly that's not very nice at all. :)

- P
Received on Tue Oct 10 08:59:16 2006