jContractor - Design By Contract

Utilisation

Introduction

Ce chapitre a pour objectif de décrire l'ensemble des règles et conventions de nommages à utiliser pour mettre en place des contrats au sein d'un programme. Dans un deuxième temps, on s'attardera à l'exécution du programme en parcourant les différents outils et options possibles qu'offre jContractor.

Précondition

Rappelons-le, cette condition doit être vérifiée par le développeur pour garantir que la suite du traitement se déroule correctement.

Considérons la signature de la méthode suivante :

            public void maMethode (Object o) {}
        

Afin d'appliquer un contrat de précondition il faut déclarer la méthode suivante :

            protected boolean maMethode_Precondition(Object o) {}
        

Le nom du contrat doit porter le même nom que la méthode sur laquelle il s'applique, suffixé par « _Precondition » et renvoyer un boolean. Les arguments de « maMethode » doivent être repris à l'identique pour le contrat.

A noter qu'on ne peut déclarer un contrat sur la méthode « Main(String[] args) », car c'est le point d'entrée du programme et on ne peut appliquer de contraintes sur ce dernier.

Concernant la visibilité de la méthode du contrat, les règles sont les suivantes :

Exemple : Prenons comme exemple la classe suivante :

            class Stack implements Cloneable {
                private Stack OLD;
                private Vector implementation;
                public Stack () { ... }
                public Stack (Object [] initialContents) { ... }
                public void push (Object o) { ... }
                public Object pop () { ... }
                public Object peek () { ... }
                public void clear () { ... }
                public int size () { ... }
                public Object clone () { ... }
                private int searchStack (Object o) { ... }
            }
        

Et voici plusieurs contrats de préconditions s'appliquant à notre classe précédente :

            protected boolean push_Precondition (Object o) {
            	return o != null;
            }
            
            private boolean searchStack_Precondition (Object o) {
            	return o != null;
            }

            //Contrat sur constructeurs
            protected boolean Stack_Precondition (Object [] initialContents)  {
            	return (initialContents != null) && (initialContents.length > 0);
            }
        

Postcondition

La postcondition est là pour garantir que le traitement de la méthode s'est bien déroulé et que la valeur de retour est conforme aux spécifications. Les règles de visibilité sont identiques à celles des contrats de Preconditions. Afin d'appliquer un contrat de postconditions, il faut déclarer la méthode suivante :

        
            protected boolean maMethode_Postcondition(Object o, Void RESULT) {}
        

Le suffixe ici devient « _Postconditions ».

Les arguments doivent être repris à l'identique de la méthode en ajoutant un dernier paramètre RESULT.

Ce dernier est typé avec le même typage que le retour de la méthode non contrat. Si la méthode ne retourne aucun résultat, on précisera le type avec la classe « Void ». Ce dernier paramètre va permettre d'effectuer des tests sur la valeur de retour de notre méthode non contrat.

Dans un contrat de Postcondition, il est essentiel de pouvoir se référer à l'état de l'objet avant son appel à la méthode, de manière à comparer l'état avant et après le traitement.

En déclarant un champ privé nommé OLD, du même typage que l'instance de la classe, on obtient cette fonctionnalité.
Il faut également implémenter l'interface « Cloneable » et la méthode « clone() », jContractor utilisera cette dernière afin de copier l'état de l'objet dans la référence OLD juste avant l'appel au contrat de postcondition.

Exemple :

			class Stack implements Cloneable {
				private Stack OLD
				...
			}
		

Exemple : On considère toujours la classe Stack, dont le code est indiqué plus haut, voici plusieurs exemples de contrats pouvant s'appliquer sur cette classe avec notamment l'utilisation du OLD et RESULT .

            protected boolean push_Postcondition (Object o, Void RESULT) {
            	return implementation.contains(o) && (size() == OLD.size() + 1);
            }
            protected boolean size_Postcondition (int RESULT) { 
	            return RESULT >= 0;
            }
        

Invariant

L'invariant permet de vérifier qu'une condition est toujours vraie. Ce contrat est un peu particulier car il ne s'applique pas à une méthode particulière, mais à l'ensemble des méthodes déclarées publiques.

A noter que le contrat d'invariance est vérifié 2 fois, en entrée et en sortie de méthode.

Voici un exemple de contrat d'Invariance :

            protected boolean _Invariant () {
        	    return size() >= 0;
            }
        

Ainsi, si on considère une méthode « maMethode », où l'on a appliqué un contrat de précondition, de postcondition et d'invariance, l'ordre de vérification des contrats est le suivant :

            public void maMethode () {
                // Vérifie l'invariant  : _Invariant()
                // Vérifie la précondition  : maMethode_Preconditon()
                
                // Contenu de la méthode
                
                // Vérifie la précondition  : maMethode_Postcondition()
                // Vérifie l'invariant en sortie  : _Invariant()
            }
        
        

En premier l'invariant est vérifié, puis la préconditions. Le traitement de la méthode est alors effectué, avant de terminer par la postcondition, et une dernière fois l'invariant.

Généralités

Voici quelques règles générales s'appliquant à tous types de contrats.

Que se passe-t-il lorsqu'un contrat échoue ?

Lorsqu'un contrat échoue, cela signifie que l'assertion a échoué et alors le contrat renvoie « false ». jContrator intercepte alors ce résultat et lancera une exception en fonction du contrats.

Type de contrat Type d'erreur
Précondition edu.ucsb.ccs.jcontractor.PreconditionViolationError
Postcondition edu.ucsb.ccs.jcontractor.PostconditionViolationError
Invariant edu.ucsb.ccs.jcontractor.InvariantViolationError

Il n'est pas recommandé de traiter les exceptions lancées par jContractor. Ces dernières sont là pour indiquer au développeur un problème à corriger au plus tôt. Il n'est donc pas logique d'effectuer un « try-catch », rappelons qu'il s'agit d'une méthode de développement et si vous êtes amenés à produire ce genre de code, c'est qu'il y a un souci dans l'écriture d'un contrat, ou dans l'utilisation des méthodes vérifié par contrat.

Héritage

Dans les sections précédentes, les contrats décrits étaient implémentés dans la même classe que le code. Cependant, jContrator offre la possibilité d'implémenter les contrats à 4 endroits différents.

Contrat interne

Les contrats sont écrits directement dans la classe où les contrats s'appliquent.

Exemple :

            public class maClasse {
                public void maMethode() { ... }
                
                protected boolean maMethode_Precondition() { ... }
                
                protected boolean maMethode_Postcondition(Void RESULT) { ... }
                
                protected boolean _Invariant() { ... }
            }
        

Contrat externe (Contrat séparé)

Le contrat est écrit dans une classe à part respectant la convention de nommage suivante :
La classe du contrat porte le même nom que la classe sur laquelle elle s'applique, et est suffixée par « _CONTRACT ».

Exemple :

            public class maClasse {
                public void maMethode() { ... }
            }
        
            public class maClasse_CONTRACT {
                protected boolean maMethode_Precondition() { ... }
                
                protected boolean maMethode_Postcondition(Void RESULT) { ... }
                
                protected boolean _Invariant() { ... }
            }
        

Remarque : Généralement on prendra soin d'hériter de la classe sur laquelle on pose les contrats.

   
            public class maClasse_CONTRACT extends maClasse {}
        

Ceci permet d'accéder directement aux champs et méthodes non privés. De cette manière on peut appeler ces derniers dans nos contrats. Autrement, sans faire du contrat, une sous classe de la classe, il est nécessaire de recréer les champs et méthode, afin de passer la compilation.

Concernant l'utilisation de champs et méthodes privés, il n'y a pas d'autre moyen que de les répéter dans la classe de contrat afin de faire un « fake » et de passer le compilateur java.

Contrat de classe mère (Super Contrat)

Les contrats sont définis dans une classe parente. Considérons une classe A qui hérite de B.

            public class B {

                public void maMethode() { ... }
                
                protected boolean maMethode_Precondition() { ... }
            }
            
            public class A extends B {

                @Override                
                public void maMethode() { ... }
            }
        

Tous les contrats définis pour « maMethode » dans B, seront aussi valables pour A si la méthode a été surchargée.

Contrat d'interface

Le principe est le même que le contrat séparé, excepté qu'il concerne les interfaces. Bien entendu, on ne peut mettre que les signatures de méthodes dans l'interface, il faut donc créer une classe avec la même convention de nommage que le contrat externe.

            public interface monInterface {
                public void maMethode();
            } 
            
            public class monInterface_CONTRACT {
                protected boolean maMethode_Precondition() { ... }
                
                protected boolean maMethode_Postcondition(Void RESULT) { ... }
                
                protected boolean _Invariant() { ... }
            }
        

Tous les contrats seront ensuite appliqués pour quiconque implémente l'interface « monInterface ».

JaQual (Java Quantification Language)

jContractor fournit un package nommé JaQual, qui a pour but de faciliter la manipulation de collections. Ce package fournit une couche d'abstraction apportant une syntaxe très verbeuse, très utile pour renforcer l'aspect documentaire de la programmation par contrat.

Voici la liste des classes ainsi que leurs descriptifs, inclus dans JaQual.

Description Exemple et Utilisation
Assertion

Interface standard de l'implémentation d'une assertion,
celle ci contient une méthode eval() avec un objet en paramètre.
							public interface Assertion {
								public boolean eval (Object o);
							}
						
Operator

Interface standard pour appliquer une transformation d'un objet.
S'utilise avec le quantifieur ForAll, cela permet d'appliquer facilement un appel
à d'autre fonction sur tous les éléments d'une collection.
							public interface Operator {
								public void execute (Object o);
							}
						
ForAll

Vérifie que tous les éléments d'une collection valide une assertion.
							Collection aCollection;
							Assertion anAssertion;
							
							ForAll.in(aCollection).ensure(anAssertion)
						
Exists

S'assure qu'au moins un élément d'une collection valide une assertion
							Exists.in(aCollection).suchThat(anAssertion)
						
Elements

Retourne un java.util.Vector contenant tous les éléments d'une
collection validant l'assertion.
							Elements.in(aCollection).suchThat(anAssertion)
						
Implies

Renvoi vrai si A et B sont tous les deux vrais, ou si A est faux.
Equivalent au « Implique » en mathématique.
							boolean A, B;
							
							Logical.implies(A, B)
						

Exemple de manipulation d'Assertion sur une collection :

		java.util.Collection nodes;
		
		//Déclaration d'une classe anonyme pour notre assertion
		Assertion connected = new Assertion () {
			public boolean eval (Object o) {
				return ((Node) o).connections >= 1;
			}
		};
		
		//On applique l'assertion avec le quantifieur ForAll sur notre Collection
		return ForAll.in(nodes).ensure(connected);
		

Exemple de manipulation d'Operator sur une collection :

			java.util.Collection elements;

			// Déclaration de notre Operator
			Operator initialize = new Operator () {
				void execute (Object o) {
					((Node) o).init();
				}
			};
			
			// On applique la transformation sur notre collection 
			// avec le quantifieur ForAll et l'Operator que l'on vient de créer
			ForAll.in(elements).execute(initialize)
		

Exécution

Nous avons vu dans les précédentes sections comment déclarer nos contrats. Cette section explique maintenant comment les exécuter.

Deux outils sont disponibles :

Autrement dit, si on exécute jInstrument puis qu'on exécute le programme sans passer par jContractor, on obtiendra la même exécution avec vérification de contrat, comme si on avait utilisé jContractor directement.

			java jInstrument --all * Foo.class
			java Foo
			// revient à faire :
			java jContractor --all * Foo
		

Pour plus d'informations sur les différentes options, se référer à la documentation officielle.

InstrumentationLevel

jContractor et jInstrument permettent de contrôler le niveau d'instrumentation. Entre autre, il est possible d'activer les contrats que sur une classe ou un package.
Ainsi, on peut spécifier une classe ou un package pour les préconditions, postconditions, ou invariants :

Rappelons que la programmation par contrat, est une méthode de développement. Il n'est pas recommandé d'appliquer les contrats sur un environnement de production.
jContractor a un impact significatif sur les performances, plus il y aura de contrats, plus l'instrumentation prendra du temps. Egalement, plus la complexité des contrats sera forte, plus l'exécution avec vérification de contrat sera longue.

Le niveau d'instrumentation, ainsi que jContractor et jInstrument permet donc de contrôler finement comment appliquer les contrats. Il est en revanche recommandé de laisser les contrats dans le code, ceci apporte une documentation supplémentaire sur le traitement et les paramètres d'une méthode.

Si toutefois, vous ne souhaitez pas conserver les contrats, l'option -s de jContractor permet de supprimer tous les contrats écrits de vos .java.
En revanche, pour supprimer l'activation des contrats dans un .class il faut recompiler.