Refinement verification via simulation S call, ret High (AIS] < call ret Low(a[O):· >>Refinement Verification Via Simulation call ret Low (A[O]): call, ret High (A[S]): e e      S O