jContractor - Design By Contract
Instrumentation
Introduction
Cette partie a pour but de décrire dans les grandes lignes, comment fonctionne jContractor en arrière plan, et quels concepts fondamentaux il est important de connaître, pour utiliser au mieux jContractor.
BCEL
jContractor est une librairie exclusivement codée en Java. La principale action de jContractor est de modifier du ByteCode afin de déplacer le code des contrats et d'effectuer leurs appels au bon endroit. Pour cela jContractor utilise la librairie BCEL (Byte Code Engineering Library) qui permet de manipuler et transformer du Byte Code depuis un programme Java.
Processus d'Instrumentation
Nous allons maintenant décrire la principale action de jContractor, qui est d'instrumenter une classe afin de modifier son code juste avant qu'elle soit chargée. Pour toutes les méthodes m, qui ne soit pas des contrats, avec une signature s, dans une classe C :
- jContractor recherche une méthode nommé m_Precondition avec une signature s,
dans la classe C ou C_CONTRACT.
Si une méthode est trouvée, on rajoute l'appel à cette méthode, au début de la méthode m. -
jContractor recherche ensuite une méthode nommé m_Postcondition avec une signature s,
ainsi qu'un argument additionnel RESULT, dans la classe C ou C_CONTRACT.
Si une méthode est trouvée, on rajoute l'appel à cette méthode, à la fin de la méthode m en ajoutant le retour de cette dernière dans l'appel au contrat. -
Si m est public, jContractor cherche une méthode _Invariant, dans la classe C ou C_CONTRACT.
Si l'invariant existe, alors l'appel à cette méthode est rajoutée, en début et fin de la méthode m.
Assertion Evaluation Rule
Une des règles de jContractor est que l'on ne vérifie qu'un contrat à la fois. Prenons pour exemple le code ci dessous :
class Stack {
public int size () { ... }
protected boolean _Invariant () {
return size() >= 0;
}
}
On a une méthode size() qui est publique, et donc lors de la vérification de contrat, le contrat _Invariant sera appelé.
Or dans notre contrat on refait appel à la méthode « size() », on a donc ici une boucle infinie.
Pour éviter ce problème, jContractor met en place « l'Assertion Evaluation Rule », qui n'est rien d'autre qu'un mécanisme de verrou.
Ainsi pendant le processus d'instrumentation, lorsque les appels au contrat seront rajoutés dans la méthode « push », jContractor prendra
le soin d'ajouter les instructions suivantes pour éviter les problèmes de concurrences et boucles infinies.
public void push (Object o) {
if (jContractorRuntime.canCheckAssertion()) {
try {
jContractorRuntime.lockAssertionCheck();
if (!_Invariant())
throw new InvariantViolationError();
if (!push_Precondition(o))
throw new PreconditionViolationError();
} finally {
jContractorRuntime.releaseAssertionCheck();
}
}
implementation.addElement(o);
if (jContractorRuntime.canCheckAssertion()) {
try {
jContractorRuntime.lockAssertionCheck();
if (!_Invariant())
throw new InvariantViolationError();
if (!push_Postcondition(o, null))
throw new PostconditionViolationError();
} finally {
jContractorRuntime.releaseAssertionCheck();
}
}
}
A noter que l'exemple ci dessus, est montré avec du code Java pour faciliter la compréhension, mais l'opération de rajouter ces instructions est effectuée directement dans le Byte Code grâce à la librairie BCEL.
Héritage
Nous avons vu dans les précédentes sections, comment étaient effectués les différents appels aux contrats, et quelles opérations étaient réalisées sur le code afin d'appliquer les contrats pendant l'exécution. Un point important n'a pas encore été discuté, rappelons qu'un contrat peut être situé à 4 endroits différents. Donc un contrat est composé au plus de 4 parties.
Imaginons le code suivant :
class A {
public void m() { ... }
protected boolean m_Postcondition(Void RESULT) { ... }
}
class B extends A implements C {
@Override
public void m() { ... }
protected boolean m_Postcondition(Void RESULT) { ... }
}
class B_CONTRACT {
protected boolean m_Postcondition(Void RESULT) { ... }
}
interface C {
void m();
}
class C_CONTRACT {
protected boolean m_Postcondition(Void RESULT) { ... }
}
On voit ici, que pour la méthode m() de B, 4 contrats sont applicables. Cette section explique comment sont assemblés les différents contrats entre eux.
La programmation par contrat implique que si une classe hérite d'une autre classe, alors tous les contrats validés dans la classe mère, doivent au moins être validés dans la classe fille.
Faisons la comparaison suivante :
On a une classe « Véhicule », avec une méthode « se déplacer », ainsi qu'une classe « Voiture »
héritant de la classe « Véhicule ». Imaginons qu'on ait
un contrat sur la méthode « se déplacer », à la fois dans « Véhicule » et « Voiture ».
Alors l'implémentation de « Voiture » doit à la fois vérifier
le contrat de « Véhicule » et de « Voiture ».
Si un contrat de Postcondition vérifie que le « Véhicule » a bougé après l'appel à la méthode « se déplacer »,
alors il est logique que la méthode « se déplacer » de « Voiture » vérifie ce contrat,
et qu'elle y ajoute ses propres spécifications, comme par exemple :
que de l'essence soit consommé.
Cette analogie a été faite pour expliquer ce qui suit :
Dans jContractor si un contrat est composé de 4 parties, alors un « ET logique »
est fait entre ces 4 contrats pour vérifier la condition.
Cette notion est valable pour les contrats de Postconditions, et d'Invariances.
Pour les contrats de Préconditions, en revanche un « OU logique » est effectué, jContractor considère que les paramètres d'entrées, selon l'implémentation, peuvent être plus spécifiques.
On peut illustrer cela par l'exemple suivant :
Pour se déplacer, une voiture ou un vélo n'utilisent pas les mêmes paramètres, l'un utilise de l'essence, l'autre
une force humaine.
En résumé la programmation par contrat implique au niveau de l'héritage que si un contrat est composé de plusieurs parties :
- Pour les contrats de postconditions et d'invariances, on effectue un « ET logique » entre tous les contrats, afin de renforcer la condition
- Pour la préconditions, du au fait de l'implémentation plus spécifique, on effectue un « OU logique » entre les différents contrats, ce qui affaiblit la condition.
La figure suivante illustre ce qui vient d'être expliqué ci-dessus. Les traits continus indiquent là ou le ByteCode est copié, tandis que les traits en pointillés indiquent là où les appels de méthode sont insérés.
