Postcondition - Postcondition

En programmation informatique , une postcondition est une condition ou un prédicat qui doit toujours être vrai juste après l'exécution d'une section de code ou après une opération dans une spécification formelle . Les postconditions sont parfois testées à l'aide d' assertions dans le code lui-même. Souvent, les postconditions sont simplement incluses dans la documentation de la section de code affectée.

Par exemple : Le résultat d'une factorielle est toujours un entier et supérieur ou égal à 1. Ainsi, un programme qui calcule la factorielle d'un nombre en entrée aurait des postconditions que le résultat après le calcul soit un entier et qu'il soit supérieur ou égal à 1. Un autre exemple : un programme qui calcule la racine carrée d'un nombre d'entrée peut avoir les postconditions que le résultat soit un nombre et que son carré soit égal à l'entrée.

Postconditions en programmation orientée objet

Dans certaines approches de conception logicielle, les postconditions, ainsi que les préconditions et les invariants de classe , sont des composants de la méthode de construction logicielle conception par contrat .

La postcondition de toute routine est une déclaration des propriétés qui sont garanties à la fin de l'exécution de la routine. En ce qui concerne le contrat de la routine, la postcondition offre l'assurance aux appelants potentiels que dans les cas où la routine est appelée dans un état dans lequel sa précondition est vérifiée , les propriétés déclarées par la postcondition sont assurées.

exemple Eiffel

L'exemple suivant écrit en Eiffel définit la valeur d'un attribut de classe en hourfonction d'un argument fourni par l'appelant a_hour. La postcondition suit le mot-clé ensure. Dans cet exemple, la postcondition garantit, dans les cas où la précondition est vérifiée (c'est-à-dire lorsque a_hourreprésente une heure valide de la journée), qu'après l'exécution de set_hour, l'attribut class houraura la même valeur que a_hour. La balise " hour_set:" décrit cette clause de postcondition et sert à l'identifier en cas de violation de postcondition à l'exécution. 

    set_hour (a_hour: INTEGER)
            -- Set `hour' to `a_hour'
        require
            valid_argument: 0 <= a_hour and a_hour <= 23
        do
            hour := a_hour
        ensure
            hour_set: hour = a_hour
        end

Postconditions et héritage

En présence d' héritage , les routines héritées par les classes descendantes (sous-classes) le font avec leurs contrats, c'est-à-dire leurs préconditions et postconditions, en vigueur. Cela signifie que toute implémentation ou redéfinition de routines héritées doit également être écrite pour se conformer à leurs contrats hérités. Les postconditions peuvent être modifiées dans des routines redéfinies, mais elles ne peuvent être que renforcées. C'est-à-dire que la routine redéfinie peut augmenter les avantages qu'elle procure au client, mais ne peut pas diminuer ces avantages.

Voir également

Les références