[abc] Concrete operational semantics

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