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
Résumé : 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.
Type de document :
Rapport
[Research Report] RR-7310, INRIA. 2010, pp.31
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00491835
Contributeur : Claude Marché <>
Soumis le : lundi 14 juin 2010 - 14:53:56
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 14:05:37

Fichier

RR-7310.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

406

Téléchargements de fichiers

167