A Refinement Approach for Correct-by-Construction Object-Oriented Programs

Asma Tafat 1, 2 Sylvain Boulmé 3 Claude Marché 1, 2
2 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-by-construction 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 language such as Java and C. 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 :
Reports
[Research Report] RR-7310, INRIA. 2010, pp.31
Liste complète des métadonnées


https://hal.inria.fr/inria-00491835
Contributor : Claude Marché <>
Submitted on : Monday, June 14, 2010 - 2:53:56 PM
Last modification on : Thursday, February 9, 2017 - 3:34:12 PM
Document(s) archivé(s) le : Friday, October 19, 2012 - 2:05:37 PM

File

RR-7310.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00491835, version 1

Collections

Citation

Asma Tafat, Sylvain Boulmé, Claude Marché. A Refinement Approach for Correct-by-Construction Object-Oriented Programs. [Research Report] RR-7310, INRIA. 2010, pp.31. <inria-00491835>

Share

Metrics

Record views

383

Document downloads

158