Skip to Main content Skip to Navigation
Conference papers

A refinement methodology for object-oriented programs

Asma Tafat 1 Sylvain Boulmé 2 Claude Marché 3 
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Refinement is a well-known approach for developing correct-byconstruction software. It has been very successful for producing high quality code e.g., as implemented in the B tool. Yet, such refinement techniques are restricted in the sense that they forbid aliasing (and more generally sharing of data-structures), which often happens in usual programming languages. We propose a sound approach for refinement in presence of aliases. Suitable abstractions of programs are defined by algebraic data types and the so-called model fields. These are related to concrete program data using coupling invariants. The soundness of the approach relies on methodologies for (1) controlling aliases and (2) checking side-effects, both in a modular way.
Document type :
Conference papers
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Friday, November 12, 2010 - 4:48:34 PM
Last modification on : Sunday, June 26, 2022 - 11:52:33 AM
Long-term archiving on: : Friday, October 26, 2012 - 3:32:07 PM


Files produced by the author(s)


  • HAL Id : inria-00534336, version 1



Asma Tafat, Sylvain Boulmé, Claude Marché. A refinement methodology for object-oriented programs. Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. pp.143--159. ⟨inria-00534336⟩



Record views


Files downloads