Re: [abc] Concrete operational semantics

Hi Eric...

You have defined a semantics fully, from the beginning. If I understand
correctly, you are asking us to confirm that it is semantically
equivalent to the abc tracematch implementation, whose (intended)
operational semantics is given in the OOPSLA 05 paper. Since you want
them to be equivalent, why not just use the semantics from the OOPSLA
paper? I see that there are some differences, such as the multiple
labelled skip loops. It would be much easier to see what is the same
and what is different (and to prove that the differences do not change
the behaviour) if the OOPSLA semantics were presented first, and then
the differences were presented as changes to the original, using the
original notation.

Ondrej

On Wed, Oct 04, 2006 at 12:10:07PM -0400, Eric Bodden wrote:
> Hi all.
>
> In the svn repository
> (https://svn.sable.mcgill.ca/sable/papers/pldi07tmstat) there is now an
> updated version, which holds a commented version of the concrete
> operational semantics for tracematches. (PDF copy attached for your
> convenience) The plan is to use this as a sort of baseline for what
> follows in the paper, i.e. the program abstraction and the actual
> analysis, which is actually really close to those operational semantics.
>
>
> I would be very grateful if everybody who was involved with the
> implementation of TMs could please try to verify that what I wrote is
> correct. In my opinion it should reflect pretty much what is actually
> going on, under the following assumptions:
>
> - Indexing and leak detection (including weak bindings) are disabled.
> (no need to bother the reader with this here)
> - Instead of a generic skip-loop we have labelled skip-loops as
> mentioned some weeks (months?) ago. See paper for details.
> - The updates in the semantics are no in-place updates but purely
> functional. Hence, we need no real "temp" data structure as in the
> actual implementation.
>
> For your convenience, I have temporarily enabled numbering of the
> equations. So if you find anything wrong, please refer to the location
> by those numbers if possible. Everything in the boxes are comments for
> you and will be replaced by an appropriate less informal filling in the
> final paper.
>
>
> Thanks a lot in advance!
>
> Cheers,
> Eric
Received on Fri Oct 06 14:10:14 2006