A weakest precondition semantics for refinement of object-oriented programs

Authors
Cavalcanti, A Naumann, DA
Citation
A. Cavalcanti et Da. Naumann, A weakest precondition semantics for refinement of object-oriented programs, IEEE SOFT E, 26(8), 2000, pp. 713-728
Citations number
34
Categorie Soggetti
Computer Science & Engineering
Journal title
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING
ISSN journal
00985589 → ACNP
Volume
26
Issue
8
Year of publication
2000
Pages
713 - 728
Database
ISI
SICI code
0098-5589(200008)26:8<713:AWPSFR>2.0.ZU;2-G
Abstract
We define a predicate-transformer semantics for an object-oriented language that includes specification constructs from refinement calculi. The langua ge includes recursive classes, visibility control, dynamic binding, and rec ursive methods. Using the semantics, we formulate notions of refinement. Su ch results are a first step toward a refinement calculus.