On Formal Analysis of OO Languages Using Rewriting Logic: Designing for Performance