Our contributions o lin. progress Pe 0 Cctxt ? P∈{PsF/PDF} New prog. properties for obj. with partial methods Abstractions to establish contextual refinements(CR)Our contributions • New prog. properties for obj. with partial methods • Abstractions to establish contextual refinements (CR) O lin. + progress P  O ctxt AP P  {PSF/PDF} ??