A Refinement Approach for Correct-by-Construction Object-Oriented Programs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2010

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

Résumé

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.
Le concept de raffinement, notion importante des méthodes formelles, permet le développement de logiciels corrects par construction. Il a été utilisé, avec succès, pour la production de code de haute qualité, par exemple, tel qu'il est implémenté dans l'atelier B. Néanmoins, de telles techniques de raffinement sont restreintes dans le sens où elles interdisent l'aliasing, et plus généralement le partage des structures de données, qui apparaît fréquemment dans les langages de programmation classiques comme C ou Java. On propose une approche sûre pour le raffinement en présence de partage. Des abstractions convenables sont définies par des types de données algébriques et ce qu'on appelle des champs modèles. Ces derniers sont reliés aux données concrêtes à l'aide d'un invariant de collage. La sûreté de notre approche s'appuie sur des méthodes pour (1) le contrôle du partage et ; (2) la gestion des effets de bord ; dans les deux cas de façon modulaire.
Fichier principal
Vignette du fichier
RR-7310.pdf (239.69 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00491835 , version 1 (14-06-2010)

Identifiants

  • HAL Id : inria-00491835 , version 1

Citer

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⟩
274 Consultations
185 Téléchargements

Partager

Gmail Facebook X LinkedIn More