A weakest precondition semantics for refinement of object-orientedprograms

摘要

We define a predicate-transformer semantics for an object orientednlanguage that includes specification constructs from refinement calculi.nThe language includes recursive classes, visibility control, dynamicnbinding, and recursive methods. Using the semantics, we formulatennotions of refinement. Such results are a first step toward a refinementncalculus