Abstraction par spécifications

Sommaire du document

Par notre spécification, nous allons décrire les relations qui existent entre les données nécessaires à l'exécution (les inputs) et le résultat atteint après l'exécution (les outputs).

Nous pouvons avoir plusieurs types de données utilisées par une procédure^[1] :

• Les paramètres de la méthode, clairement définis dans la signature de méthode, sont des inputs explicites.
• La méthode peut faire appel à d'autres données, comme par exemple une entrée standard (valeur introduite à l'aire du clavier), la lecture d'un fichier, etc. Nous n'avons aucune indication de l'existance et de l'utilisation de ces données en lisant simplement la signature de la méthode. Ce sont des inputs implicites.

Procédures totales et partielles

Avant de continuer, nous devons envisager le contexte dans lequel notre procédure sera exécutée. En “software engineering”^[2] nous utilisons le terme « fiabilité » (en anglais, “reliability”) pour dire que l'exécution est possible dans toutes les conditions possibles. Dans le cas de l'abstraction par spécification, nous utiliserons les qualificatifs total et partiel :

• Si nous avons défini le comportement de la procédure pour tout type d'input en accord avec la signature de la procédure, notre spécification en fait une procédure totale. Peu importe ce qui sera fourni en entrée pouvu que la signature soit respectée, nous garantissons le résultat attendu de la procédure.
• Dans le cas oû le fonctionnement de la procédure est soumis à certaines conditions d'entrées, nous sommes face à une procédure partielle. Notre spécification doit donc comporter une clause "require", et si cette clause n'est pas respectée le résultat de l'exécution de la procédure est totalement indéfini et hors de notre responsabilité.

Clauses de la spécification

Requires

Requires permet de définir les contraintes (pré-conditions) nécessaires pour garantir le résultat attendu. Requires est une clause optionnelle.

Nous avons vu que la présence de la clause "require" implique que la procédure soit partielle, et dans certains cas cela permet d'en optimiser l'exécution. Par exemple, une recherche dans un tableau peut spécifier que le tableau doit être trié pour que la procédure nous donne le résultat escompté^[4].

Modifies

Modifies permet de définir quelles sont les données qui sont suceptibles d'être modifiées lors de l'exécution. Modifies est une clause optionnelle.

Si nous sommes en présence d'une clause "modifies" dans notre spécification, et que cette clause n'est pas vide, nous parlons d'« effets de bord » (en anglais, “side effects”).

Effects

Effects permet de définir le comportement attendu, et le résultat de ce comportement (post-conditions). Effects est une clause obligatoire, car la signature d'une méthode n'est pas toujours suffisante pour en déduire ces informations.

La clause "effects" ne porte que sur le comportement attendu lors de l'exécution de la procédure sans clause "requires", ou en accord avec la clause "requires" si elle existe. Le comportement dans le cas ou "requires" n'est pas respecté ne doit pas figurer dans la clause "effects".

Comme l'exécution de la procédure est suceptible de modifier certaines données, nous pouvons différencier la donnée avant et aprè l'exécution. Différentes possibilités existent, et nous pouvons par exemple utiliser des suffixes tels que _pre et _post.

De méme, si la procédure retourne une nouvelle donnée (par exemple un nouvel objet) qui prète à confusion avec un des inputs, nous devons spécifier dans la clause "effects" qu'il s'agit d'un "nouveau".

Spécifications sous-déterminées

Lorsque nous savons que l'exécution d'une procédure avec un même input peut avoir plus d'un résultat possible (chaque résultat respectant les spécifications), nous parlons de « spécification sous-déterminée » (en anglais, “undetermined specification”).

Généralement, une spécification sous-déterminée est implémentée de manière déterministe (l'exécution de la procédure avec un même input retournera toujours la même chose), sauf dans le cas où la clause "effects" stipule que le résultat doit être différent (incrémentation, aléatoire, etc.).

Rendre totale une procédure partielle

Pour rendre totale une procédure partielle, nous pouvons supprimer la clause requires, et spécifier dans la clause effects une valeur de retour bien définie, qui signifie que l'exécution à échoué, ou n'est pas garantie. Ce genre de comportement n'est toutefois pas toujours possible (par exemple si toutes les valeurs de l'ensemble associé au type de retour sont suceptibles de faire partie du résultat).

Une autre manière de procéder est l'utilisation des exceptions. Dans ce cas, les exceptions qui peuvent être lancées dans un cadre respectant la clause requires doivent figurer dans la signature^[7].

Nous distinguons en Java deux grands types d'exceptions :

• Les “unchecked exceptions”^[8] sont des exceptions qui ne doivent normalement pas se produire (par exemple, quelque chose que le code appelant peut facilement vérifier). La déclaration des exceptions non vérifiées ne fait pas partie de la signature.
• Les “checked exceptions”^[9] sont des exceptions qui peuvent se produire (par exemple, une coupure du réseau, une erreur matérielle). La déclaration des exceptions vérifiées faitpartie de la signature.

Java n'impose pas de renseigner la possibilité de lancer une exception non vérifiée, mais dans certains cas c'est une bonne pratique de les spécifier.

Une autre bonne pratique est l'utilisation d'une FailureException (exception non vérifiée) dans le cas où la procédure est exécutée en violant une clause requires. Nous ne devrons pas renseigner cette exception dans effects car elle est implicite de par la cause require.

Notes

1. ↑ Procédure : Nous utilisons ici le terme procédure, mais nous pouvons le remplacer par méthode, fonction, etc.
   
   
2. ↑ software engineering : correspond à « génie logiciel” en français
   
   
3. ↑ fiabilité : correspond à “reliability » en anglais
   
   
4. ↑ Programmation défensive : Nous pouvons implémenter le code de telle manière que dès que la recherche détecte que le tableau n'est pas trié un tri du tableau soit effectué avant de reprendre la recherche. Dans ce cas, nous devons retirer la nécessité d'un tableau trié dans la clause requires, et ajouter un commentaire stipulant que le travail est plus long si le tableau n'est pas trié.
   
   
5. ↑ effets de bord : correspond à “side effects » en anglais
   
   
6. ↑ spécification sous-déterminée : correspond à “undetermined specification » en anglais
   
   
7. ↑ Signature et exceptions : En Java, la déclaration des exceptions non vérifiées ne fait pas partie de la signature, au contraire des exception vérifiées qui doivent y figurer.
   
   
8. ↑ unchecked exceptions : correspond à « exceptions non vérifiées” en français
   
   
9. ↑ checked exceptions : correspond à « exceptions vérifiées” en français
   
   

Structure du document