Reasoning about Object Behaviours with Rewriting.
Résumé
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.