A weakest precondition semantics for an object-oriented language of refinement

Ana Cavalcanti, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

21 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 towards a refinement calculus.

Original languageEnglish
Title of host publicationFM 1999 - Formal Methods - World Congress on Formal Methods in the Development of Computing Systems, Proceedings
EditorsJeannette M. Wing, Jim Woodcock, Jim Davies
Pages1439-1459
Number of pages21
DOIs
StatePublished - 1999
Event1st World Congress on Formal Methods in the Development of Computing Systems, FM 1999 - Toulouse, France
Duration: 20 Aug 199924 Aug 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1709
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference1st World Congress on Formal Methods in the Development of Computing Systems, FM 1999
Country/TerritoryFrance
CityToulouse
Period20/08/9924/08/99

Keywords

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

Fingerprint

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

Cite this