Reasoning about Object Behaviours with Rewriting.

Adel Bouhoula 1 Ahmed Jebali 1 Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Observational specification techniques are well adapted to the description of object-oriented systems where non observable sorts are used to model the states of objects, and states can be observed only by applying methods on their attributes. In this setting, reasoning about objects requires that we are able to prove or disprove behavioural satisfaction of equations. This is the problem we propose to solve here through an extension of equational rewriting techniques. We also address the related problem of refinement in object-oriented specifications and use the same techniques to show that a concrete class behaviourally satisfies the properties of an abstract one.
Mots-clés : objets refinement objects behaviours proofs comportements preuves raffinement
Type de document :
Communication dans un congrès
Workshop on Object-Oriented Specification Techniques for Distributed Systems and Behaviours (in conjunction with Principles, Logics, and Implementations of high-level programming languages PLI99) - OOSDS'99, 1999, Paris, France, 6 p, 1999
Liste complète des métadonnées
https://hal.inria.fr/inria-00099000
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:41:07
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00099000, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Adel Bouhoula, Ahmed Jebali, Michaël Rusinowitch. Reasoning about Object Behaviours with Rewriting.. Workshop on Object-Oriented Specification Techniques for Distributed Systems and Behaviours (in conjunction with Principles, Logics, and Implementations of high-level programming languages PLI99) - OOSDS'99, 1999, Paris, France, 6 p, 1999. 〈inria-00099000〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

262

Contact


archive-ouverte@inria.fr