Abstractions contextual refinements Contextual Refinement(CR) o Ctx A iff VC. Obs Beh(c[o1)c Obs Beh(C[A]) void acq i Concrete Client c object o while(truer void relOt acq aca print(1) relo acq Is o as good as A, Abstract rel from Cs point of view? object aAbstractions & Contextual Refinements O ctxt A iff C. ObsBeh(C[O])  ObsBeh(C[A]) Contextual Refinement (CR): Is O as good as A, from C’s point of view?