Contextual refinement as OS Correctness O Ectxt s iff V A. ObsBeh (A[)c ObsBeh (A[sT The set of observable behaviors A: Application O: OS Concrete Impl. S: Abstract PrimContextual Refinement as OS Correctness The set of observable behaviors A：Application O：OS Concrete Impl. S：Abstract Prim. O ctxt S iff A. ObsBeh(A[O])  ObsBeh(A[S])