Forward simulation for data refinement of classes

Ana Cavalcanti, David A. Naumann

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

18 Scopus citations

Abstract

Simulation is the most widely used technique to prove data refinement. We define forward simulation for a language with recursive classes, inheritance, type casts and tests, dynamic binding, class based visibility, mutable state (without aliasing), and specification constructs from refinement calculi. It is a language based on sequential Java, but it also includes specification and deseign mechanisms appropriate for the construction of programs based on refinement. We show simulation to be sound for data refinement of classes in this language.

Original languageEnglish
Title of host publicationFME 2002
Subtitle of host publicationFormal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings
EditorsLars-Henrik Eriksson, Peter Alexander Lindsay
Pages471-490
Number of pages20
ISBN (Electronic)9783540439288
DOIs
StatePublished - 2002
Event11th International Symposium of Formal Methods Europe, FME 2002 - Copenhagen, Denmark
Duration: 22 Jul 200224 Jul 2002

Publication series

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

Conference

Conference11th International Symposium of Formal Methods Europe, FME 2002
Country/TerritoryDenmark
CityCopenhagen
Period22/07/0224/07/02

Keywords

  • Data refinement
  • Object-orientation
  • Program analysis and verification
  • Soundness of simulation

Fingerprint

Dive into the research topics of 'Forward simulation for data refinement of classes'. Together they form a unique fingerprint.

Cite this