WP Semantics for OO Programs and Its Applications I
Liu Yingjing, Zongyan Qiu · 2012
For the object oriented (OO) world, developing formal semantics for theoretical study and practical use is still an important topic despite of a decade’s e orts. In this paper, for a su ciently large subset of sequential Java with a pure reference semantics model, we define a Weakest Precondition (WP) semantics, and prove its soundness and completeness. Based on this WP semantics, we study specifications of methods and the refinement relationship between specifications, and we propose new definitions for object invariants and behavioral subtyping notation for general OO programs.