[PRL] legacy code and AOP

[Shriram Krishnamurthi]

Karl,

Interesting comment, but I view your (3) as a *refinement* of (2), not
different from (or merely "related" to) it.  In particular, we would
like aspects to refine rather than drastically alter the program's
behavior.  Unfortunately, of course, this has proven rather hard to
capture semantically.  This idea, as you know, is at the very heart of
our verification technique -- and the proof has correspondingly been
rather daunting (but it exists, fear not).

Shriram