A weakest precondition semantics for refinement of object-oriented programs

Ana Cavalcanti; David A. Naumann

doi:10.1109/32.879810

A weakest precondition semantics for refinement of object-oriented programs

Ana Cavalcanti
, David A. Naumann

Department of Computer Science

IEEE
Stevens Institute of Technology

Research output: Contribution to journal › Article › peer-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 language	English
Pages (from-to)	713-728
Number of pages	16
Journal	IEEE Transactions on Software Engineering
Volume	26
Issue number	8
DOIs	https://doi.org/10.1109/32.879810
State	Published - 2000

Keywords

Object-orientation
Refinement calculi
Semantic models
Verification

Access to Document

10.1109/32.879810

Cite this

@article{0ce0074b146f43dca93b628b984f87d6,

title = "A weakest precondition semantics for refinement of object-oriented programs",

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.",

keywords = "Object-orientation, Refinement calculi, Semantic models, Verification",

author = "Ana Cavalcanti and Naumann, \{David A.\}",

year = "2000",

doi = "10.1109/32.879810",

language = "English",

volume = "26",

pages = "713--728",

number = "8",

}

TY - JOUR

T1 - A weakest precondition semantics for refinement of object-oriented programs

AU - Cavalcanti, Ana

AU - Naumann, David A.

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

KW - Object-orientation

KW - Refinement calculi

KW - Semantic models

KW - Verification

UR - https://www.scopus.com/pages/publications/0034245206

UR - https://www.scopus.com/pages/publications/0034245206#tab=citedBy

U2 - 10.1109/32.879810

DO - 10.1109/32.879810

M3 - Article

AN - SCOPUS:0034245206

SN - 0098-5589

VL - 26

SP - 713

EP - 728

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

IS - 8

ER -

A weakest precondition semantics for refinement of object-oriented programs

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this