A weakest precondition semantics for refinement of object-oriented programs

Ana Cavalcanti, David A. Naumann

Research output: Contribution to journalArticlepeer-review

38 Scopus citations

Abstract

We define a predicate-transformer semantics for an object-oriented language that includes specification constructs from refinement calculi. The language includes recursive classes, visibility control, dynamic binding, and recursive methods. Using the semantics, we formulate notions of refinement. Such results are a first step toward a refinement calculus.

Original languageEnglish
Pages (from-to)713-728
Number of pages16
JournalIEEE Transactions on Software Engineering
Volume26
Issue number8
DOIs
StatePublished - 2000

Keywords

  • Object-orientation
  • Refinement calculi
  • Semantic models
  • Verification

Fingerprint

Dive into the research topics of 'A weakest precondition semantics for refinement of object-oriented programs'. Together they form a unique fingerprint.

Cite this