Our contributions O lin. progress Pe 0 Cctxt Ap P∈{PsF/PDF} New prog. properties for obj. with partial methods Abstractions to establish contextual refinements(CR) Equivalence result(Abstraction Theorem) Program logic for Progress Reasoning Linearizability + PSF/PDFOur contributions • New prog. properties for obj. with partial methods • Abstractions to establish contextual refinements (CR) • Equivalence result (Abstraction Theorem) • Program logic for Progress Reasoning • Linearizability + PSF/PDF O lin. + progress P  O ctxt AP P  {PSF/PDF}