Abstraction par spécifications

Inhoudsopgave

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é.

Inhoudsopgave Haut

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".

Inhoudsopgave Haut

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.).

Inhoudsopgave Haut

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.

Nederlandse vertaling

U hebt gevraagd om deze site in het Nederlands te bezoeken. Voor nu wordt alleen de interface vertaald, maar nog niet alle inhoud.

Als je me wilt helpen met vertalingen, is je bijdrage welkom. Het enige dat u hoeft te doen, is u op de site registreren en mij een bericht sturen waarin u wordt gevraagd om u toe te voegen aan de groep vertalers, zodat u de gewenste pagina's kunt vertalen. Een link onderaan elke vertaalde pagina geeft aan dat u de vertaler bent en heeft een link naar uw profiel.

Bij voorbaat dank.

Document heeft de 31/12/2009 gemaakt, de laatste keer de 26/10/2018 gewijzigd
Bron van het afgedrukte document:https://www.gaudry.be/nl/programmer-abstraction-specifications.html

De infobrol is een persoonlijke site waarvan de inhoud uitsluitend mijn verantwoordelijkheid is. De tekst is beschikbaar onder CreativeCommons-licentie (BY-NC-SA). Meer info op de gebruiksvoorwaarden en de auteur.

Notes
  1. ↑ Procédure : Nous utilisons ici le terme procédure, mais nous pouvons le remplacer par méthode, fonction, etc.

  2. ↑ software engineering : komt overeen met « génie logiciel » en français

  3. ↑ fiabilité : komt overeen met “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 : komt overeen met “side effects” en anglais

  6. ↑ spécification sous-déterminée : komt overeen met “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 : komt overeen met « exceptions non vérifiées » en français

  9. ↑ checked exceptions : komt overeen met « exceptions vérifiées » en français

Inhoudsopgave Haut