6 Conception par Contrats et Assertions

Si les classes sont destinées à être définies comme des mises en oeuvre de type de données abstraites, on doit ne doit pas les connaître juste par les opérations disponibles, mais aussi par les propriétés formelles de ces opérations, qui ne sont pas encore apparu dans l'exemple précédent.

Le role des assertions

Eiffel encourage les développeurs de logiciels à exprimer les propriétés formelles des classes en écrivant des assertions, (NDT: en français assertion peut se traduire par affirmation, je ne traduit toutefois pas le mot dans le reste du texte) qui peuvent en particulier avoir les rôles suivants :

• Les conditions préalables (NDT: preconditions) d'une routine expriment les exigences que les clients doivent satisfaire chaque fois qu'ils appellent une routine. Par exemple le designer de ACCOUNT peut vouloir permettre une opération de retrait seulement si cela garde le solde du compte à ou au-dessus du minimum. Les conditions préalables sont introduites par le mot-clé require.
  
• Les postconditions d'une routine, introduites par le mot-clé ensure, expriment des conditions que la routine (le fournisseur) garantit sur le retour, si la condition préalable a été satisfaite sur l'entrée.
  
• Un invariable (NDT: invariant) d'une classe doit être satisfait par chaque instance de la classe chaque fois que l'instance est extérieurement accessible : après création et après n'importe quel appel à une routine exportée de la classe. L'invariable apparaît dans une clause introduite par le mot-clé invariant et représente une contrainte de cohérence générale imposée à toutes les routines de la classe.

Avec des assertions appropriées, la classe ACCOUNT devient:

class ACCOUNT
create
make
feature
... Attributes as before:
balance , minimum_balance , owner , open ...
deposit (sum: INTEGER) is
-- Deposit sum into the account.
require
sum >= 0
	do
add (sum)
ensure
balance = old balance + sum
end
withdraw (sum: INTEGER) is
-- Withdraw sum from the account.
require
sum >= 0
	sum <= balance - minimum_balance
do
add (-sum)
ensure
balance = old balance - sum
end
may_withdraw ... -- As before
feature {NONE}
add ... 

	make (initial: INTEGER) is
-- Initialize account with balance initial.
require
initial >= minimum_balance
do
balance := initial
end
invariant
balance >= minimum_balance
end -- ACCOUNT

La notation old expression est seulement valide dans une postcondition de routine. Elle signifie la valeur que l'expression avait à l'entrée de la routine.

Procédures de création

Dans sa dernière version ci-dessus, la classe inclut maintenant une procédure de création, make. Avec la première version, les clients ont utilisé des instructions de création comme create acc1 pour créer des comptes; mais alors l'initialisation par défaut, mettant le solde à zéro, a violé l'invariable. En ayant une ou plusieurs procédures de création, listées dans la clause create au début du code de la classe, une classe offre une façon de passer outre les initialisations par défaut.

L'effet de

create acc1.make (5_500)

est d'allouer l'objet (comme avec la création par défaut) et d'appeler la procédure make sur cet objet, avec l'argument donné. L'appel est correct puisqu'il satisfait la precondition; il garantira l'invariable.

Le underscore _ dans la constante entière 5_500 n'a pas d'effet sémantique. La règle générale est que vous pouvez grouper les chiffres par jeux de trois depuis la droite pour améliorer la lisibilité des constantes entières.

Notez que le même mot-clé, create, sert aussi bien à présenter des instructions de création que pour la clause de la liste des procédures de création au début de la classe.

Une procédure inscrite dans la clause de création, comme make, utilise autrement les mêmes propriétés que les autres routines, particulièrement pour les appels. Ici la procédure make est secrète puisqu'il apparaît dans une clause commençant avec feature { NONE } ; Donc il serait invalide pour un client d'inclure un appel comme

acc.make (8_000)

Pour rendre un tel appel valide, il suffirait de déplacer la déclaration de make à la première clause feature de la classe ACCOUNT, qui ne porte aucune restriction d'exportation. Un tel appel ne crée pas de nouvel objet, mais réinitialise simplement le solde d'un compte précédemment créé.

Conception par Contrat (Design by Contract™)

Syntaxiquement, les assertions sont des expressions booléennes, avec quelques extensions comme la notation old. Aussi, vous pouvez diviser une affirmation dans deux clauses ou plus, comme ici avec la précondition de withdraw; c'est comme si vous aviez séparé les clauses avec un and, mais en rendant l'affirmation plus claire, particulièrement si elle inclut beaucoup de conditions.

Les assertions jouent un rôle central dans la méthode Eiffel pour construire un logiciel orienté objet fiable. Elles servent à rendre explicite les suppositions sur lesquelles les programmeurs comptent quand ils écrivent des éléments logiciels qu'ils croient être correct. L'écriture d'assertions revient à expliquer clairement les termes du contrat qui dirige la relation entre une routine et ses appelants. La précondition créer une obligation pour les appelants; la postcondition créer une obligation pour la routine.

La théorie sous-jacente de Conception par Contrat ™, la pièce maîtresse de la méthode Eiffel, considère la construction logicielle comme basé sur des contrats entre des clients (des appelants) et des fournisseurs (des routines), comptant sur les obligations mutuelles et les avantages rendus explicites par les assertions.

Le formulaire de Contrat (Contract Form)

Les assertions sont aussi un outil indispensable pour la documentation de composants logiciels réutilisables : on ne peut pas s'attendre à la réutilisation à grande échelle sans une documentation précise de ce que chaque composant attend (la précondition), ce qu'il garantit en retour (la postcondition) et quelles conditions générales il maintient (invariable).

Les outils de documentation dans EiffelStudio utilisent des assertions pour produire des informations pour les programmeurs des clients, décrivant les classes en termes de comportement observable, pas de mise en oeuvre. En particulier le Formulaire de Contrat d'une classe, aussi appelée son "formulaire court" ("short form"), qui sert à la documentation de son interface, est obtenue à partir du texte intégral en enlevant toutes ses caractéristiques non-exportées et toutes les informations de mise en oeuvre comme les clauses do des routines, mais en gardant les informations d'interface et en particulier les assertions. Voici le Formulaire de Contrat de la classe ci-dessus:

 interface ACCOUNT
create
make
feature
balance: INTEGER
...
deposit (sum: INTEGER) is
-- Deposit sum into the account.
require
sum >= 0
	ensure
balance = old balance + sum
withdraw (sum: INTEGER) is
-- Withdraw sum from the account.
require
sum >= 0
	sum <= balance - minimum_balance
ensure
balance = old balance - sum
may_withdraw ...

end -- ACCOUNT

Ce n'est pas du Eiffel réel, seulement la documentation de classes Eiffel, d'où l'utilisation d'une syntaxe légèrement différente pour éviter toute confusion (interface class plutôt que class). Conformément au Principe d'Accès Uniforme (Uniform Access Principle) (page 7), la sortie pour balance (solde) serait la même si cette fonctionnalité était une fonction plutôt qu'un attribut.

Vous trouverez dans EiffelStudio des outils automatiques pour produire le Formulaire de Contrat (Contract Form) d'une classe. Vous pouvez aussi obtenir le formulaire de Contrat Plat (Flat Contract form), basée sur les mêmes idées, mais incluant des fonctionnalités héritées avec ceux introduits dans la classe elle-même. EiffelStudio peut produire ces formulaires et d'autres vues de documentation d'une classe, dans une variété de formats de sortie incluant le HTML, pour que des projets faits en collaboration puissent automatiquement distribuer les dernières versions de leur classe sur Internet ou Intranet.

Des contrats pour tester et débuguer

Sous EiffelStudio vous pouvez aussi configurer des options de compilation, pour le système entier ou pour des classes spécifiques seulement, afin d'évaluer les assertions à l'exécution, pour découvrir des erreurs potentielles ("bugs"). EiffelStudio fournit plusieurs niveaux de contrôle des assertions: préconditions seulement, postconditions etc. Quand le contrôle est en fonction, une assertion évaluée à vrai n'a aucun effet sur l'exécution. Une assertion évaluée à faux déclenchera une exception, comme décrit plus loin; à moins que vous n'ayez écrit un gestionnaire (handler) d'exception approprié, l'exception causera un message d'erreur et une terminaison avec un message précis et une trace d'appel.

Cette capacité de vérifier des assertions fournit un mécanisme de test et de débogage puissant, en particulier parce que les classes des Bibliothèques EiffelBase, largement utilisées dans le développement logiciel Eiffel, sont protégées par des assertions soigneusement écrites.

Le contrôle de l'exécution est, cependant, seulement une utilisation des assertions, dont le rôle comme la conception et les aides de  documentation, en tant que partie de la théorie de Conception par Contrat, exerce une influence générale sur le style Eiffel de développement logiciel.