No cache version.
Caching disabled. Default setting for this page:enabled (code LNG204)If the display is too slow, you can disable the user mode to view the cached version.
Abstraction par spécifications
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édure1 :
- 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 signature7.
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.
English translation
You have asked to visit this site in English. For now, only the interface is translated, but not all the content yet.If you want to help me in translations, your contribution is welcome. All you need to do is register on the site, and send me a message asking me to add you to the group of translators, which will give you the opportunity to translate the pages you want. A link at the bottom of each translated page indicates that you are the translator, and has a link to your profile.
Thank you in advance.
Document created the 31/12/2009, last modified the 26/10/2018
Source of the printed document:https://www.gaudry.be/en/programmer-abstraction-specifications.html
The infobrol is a personal site whose content is my sole responsibility. The text is available under CreativeCommons license (BY-NC-SA). More info on the terms of use and the author.
Notes
- ↑ Procédure : Nous utilisons ici le terme procédure, mais nous pouvons le remplacer par méthode, fonction, etc.
- ↑ software engineering : corresponds to « génie logiciel » en français
- ↑ fiabilité : corresponds to “reliability” en anglais
- ↑ 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é.
- ↑ effets de bord : corresponds to “side effects” en anglais
- ↑ spécification sous-déterminée : corresponds to “undetermined specification” en anglais
- ↑ 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.
- ↑ unchecked exceptions : corresponds to « exceptions non vérifiées » en français
- ↑ checked exceptions : corresponds to « exceptions vérifiées » en français
