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.
Type de document :
Communication dans un congrès
Bernhard Beckert and Claude Marché. Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. Karlsruhe University, 2010-13, pp.143--159, 2010, Karlsruhe Reports in Informatics; Formal Verification of Object-Oriented Software, Papers Presented at the International Conference


https://hal.inria.fr/inria-00534336
Contributeur : Claude Marché <>
Soumis le : vendredi 12 novembre 2010 - 16:48:34
Dernière modification le : jeudi 9 février 2017 - 15:54:54
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:32:07

Fichier

13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00534336, version 1

Collections

Citation

Asma Tafat, Sylvain Boulmé, Claude Marché. A refinement methodology for object-oriented programs. Bernhard Beckert and Claude Marché. Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. Karlsruhe University, 2010-13, pp.143--159, 2010, Karlsruhe Reports in Informatics; Formal Verification of Object-Oriented Software, Papers Presented at the International Conference. <inria-00534336>

Partager

Métriques

Consultations de
la notice

228

Téléchargements du document

140