Partage
  • Partager sur Facebook
  • Partager sur Twitter

[metho] Post condition/Invariant

Sujet résolu
    11 mai 2019 à 8:20:29

    Bonjour.

    Je me permets de ré-ouvrir un vieux sujet:

    https://openclassrooms.com/forum/sujet/programation-par-contrat-l-utilisez-vous

    Depuis que j'ai ouvert ce sujet, j'ai utilisé les pré-conditions (intensivement!) [ça me parait maintenant indispensable], l'objectif principal étant de vérifier les arguments (voir les variables membres) au lancement des fonctions.

    Mais je me rends compte que je n'ai jamais réutilisé les Post-conditions et les Invariants. En effet, comme <Voeux pieux> "mon code n'est pas bugger" </voeux pieux>, il n'y a pas de raison de tester mes valeurs de retour, ou les variables membres au milieux des fonctions.

    Auriez-vous des exemples qui pourrait m'aider à identifier l'utilité des Post-condition et des Invariants ?

    Merci d'avance.

    • Partager sur Facebook
    • Partager sur Twitter
      11 mai 2019 à 9:11:44

      S'assurer que la fonction fait effectivement ce qu'elle est censée faire ^^ Imaginons que j'ai une fonction censée me renvoyer un entier positif supérieur à disons 12. J'ai une post-condition évidente, la valeur retournée doit être supérieure à 12, si le test de post-condition échoue, c'est que la fonction est buggée. Autre exemple, si j'ajoute un ensemble d'éléments à une collection, la taille de la collection doit augmenter exactement du nombre d'éléments ajoutés.
      • Partager sur Facebook
      • Partager sur Twitter
      Mettre à jour le MinGW Gcc sur Code::Blocks. Du code qui n'existe pas ne contient pas de bug
        11 mai 2019 à 13:33:57

        En général, on vérifie les post-conditions à l'aide des test unitaires. Cela dit ça n'interdit pas de mettre une assertion en fin de fonction pour vérifier que l'on respecte bien la post-condition prévue. Par contre ça va souvent avoir tendance à dépendre des données d'entrée donc dans le code de la fonction elle-même, ça peut vite alourdir (surtout s'il y a mutation), donc généralement, on préfère que ce soit fait dans les tests de la fonction (ou à travers un preuve formelle :ange:).

        Pour les invariants, c'est très variable, parce qu'il y en a beaucoup de catégories. Pour les invariants de boucle c'est généralement pas nécessaire. En revanche, un invariant d'objet, dans les faits, ça représente une précondition qui doit être vraie pour tout appel jusqu'à la destruction (et donc établie par la construction et maintenue par chaque méthode). Donc pour le coup, vérifier la préservation à la fin de chaque appel peut se montrer très pratique : c'est nécessairement le code de la classe qui fout la merde dans un tel cas (sinon c'est que les contrôles de précondition sont insuffisants).

        -
        Edité par Ksass`Peuk 11 mai 2019 à 13:35:34

        • Partager sur Facebook
        • Partager sur Twitter

        Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C

          11 mai 2019 à 23:03:19

          Bonsoir et merci pour ces réponses.

          Pour faire court, ça correspond (presque) à ce que je pensais.

          Merci encore.

          PS:

          Ksass`Peuk a écrit:

          ... donc généralement, on préfère que ce soit fait [...]   à travers un preuve formelle :ange:).

          ( Tient, ça me rappel une soutenance :-°   )
          • Partager sur Facebook
          • Partager sur Twitter
            12 mai 2019 à 13:04:53

            Salut,

            Déjà, bien souvent, on se rend compte que la post condition d'une fonction devient très rapidement la pré condition d'une autre.

            Car le principe de toute fonctionnalité est qu'elle ne prend réellement du sens que... par l'usage que l'on peut en faire, et si une fonctionnalité impose une post condition, c'est que la donnée sur laquelle se base cette condition sera... utilisée "par ailleurs".

            Il y a donc "de très fortes chances" pour que, dans le cadre d'une utilisation "normale" de ta fonction, cette post condition soit testée au travers d'une pré condition.

            Mais tu le sais aussi bien que moi, la chance n'existe pas en programmation : seule la malchance existe :D

            On ne peut donc pas compter sur la chance pour que cette post condition soit testée de manière systématique (ne serait-ce que dans le cadre d'une politique correcte de tests unitaires, par exemple).

            D'un autre coté, si les préconditions nécessaires à l'exécution d'une fonction sont remplies (et donc que tu les as correctement testées au travers d'une assertion :D ), posons nous la question des raisons pour lesquelles la post condition pourrait ne pas l'être.

            Je vois deux raisons à cela :

            • Soit la logique de ta fonction n'est pas correcte,
            • soit il s'est passé "un événement imprévu" lors de l'exécution de la logique

            Si c'est due à une logique incorrecte, il n'y a rien à faire : la logique devra impérativement être corrigée avant de passer en production.  Mais cela ne veut absolument pas dire qu'il n'y a aucun risque de voir survenir un "événement imprévu".

            Du moins, dans une approche strictement générale, sans savoir ni ce que doit faire la fonction, ni les données qu'elle est sensée manipuler ou dont elle a besoin pour fournir le résultat attendu ;)

            Dans certains cas, on peut décemment se dire que, si la post condition n'est pas remplie, c'est que nous sommes face à une erreur de logique. Par exemple :

            int add(int a, int b){
                 /* vérification des pré conditions : a et b
                  * doit être compris entre 1 et 10 et
                  * et b doit être compris entre 11 et 20
                  */
                 assert(a>=1 && a< 10 && "invalid a value");
                 assert(b>=11 && b< 20 && "invalid b value");
                 auto result = a * b;
                 /* du fait des pré conditions, la post condition est
                  * que le résultat est compris entre 12 et 28
                  */
                 assert(result>=12 && resul <29 && "what did you do?");
                return result;
            }

            j'ai volontairement placé des pré et des post conditions "taillées sur mesure" pour bien montrer le fait que seule la logique (je multiplie au lieu d'additionner, c'est ballot hein ? :D ) risque de poser problème à partir du moment où les pré conditions sont remplies.

            Dans un cas pareil, il semble cohérent d'utiliser une assertion, car il n'y a pas la moindre possibilité d'être confronté à un "événement imprévu".

            Dans tous les autres cas (comprends : dés qu'un "événement imprévu" risque d'empêcher notre fonction de fournir le résultat attendu), la règle est de mettre fin au comportement de la fonction "le plus tôt possible",et donc, dés qu'on se rend compte qu'il sera impossible de fournir le résultat attendu.

            Par exemple, si on veut accéder au contenu d'un fichier, on "court toujours le risque" que le fichier ne soit pas accessible: c'est -- très clairement -- la première raison pour laquelle la fonction ne pourrait pas fournir le résultat attendu.

            Et cette situation doit être prise en compte "tout de suite après la tentative d'ouverture du ficher, mais elle n'a absolument rien à voir avec un problème de logique quelconque.

            Nous commencerions donc sans doute avec une fonction

            std::vector<UnType> readFile(std::string const & filename){
                std::ifstream ifs(filename);
                if(! ifs){
                    throw std::runtime_error("unable to open file");
                }
            }

            parce qu'il est parfaitement cohérent d'empêcher la fonction d'aller lire dans un fichier ... auquel elle n'a pas accès.

            La question que l'on pourrait se poser, c'est "oui, mais pourquoi lancer une exception et non utiliser une assertion ?"

            La réponse tient en trois raisons:

            • La première, c'est que les assertions seront supprimées de l'exécutable final (de production), et qu'il se peut que le fichier soit accessible sur l'ordinateur de développement et inaccessible sur l'ordinateur de production.
            • La deuxième est que la résolution du problème (demander confirmation du nom, par exemple) ne pourra pas se faire au niveau de la fonction readFile
            • Et, pire que tout : il se peut qu'il n'y ait aucune tentative de résolution du problème, ou, du moins qu'aucune tentative pour le résoudre ne réussisse.

            La meilleure solution est donc très clairement de faire planter le programme (en expliquant "pourquoi il a planté"), car le fait de le faire continuer à fonctionner "envers et contre tout" produirait des résultats catastrophiques.

            L'étape suivante dans le développement de cette fonction consistera à ... lire le contenu du fichier, et à remplir un tableau de UnType avec les données que l'on va en extraire.

            Mais, là encore, nous sommes confrontés à un problème auquel nous ne pouvons rien et que l'on ne peut pourtant pas ignorer : le contenu du fichier peut être corrompu.

            Les même cause ayant les mêmes effets (il n'est pas du ressort de la fonction readFile d'essayer de corriger les données qu'elle extrait: si elle tombe sur une donnée invalide, il vaut mieux "laisser planter l'application"), l'extraction des données doit provoquer une exception si les données sont invalides, ce qui nous amènerait à une fonction proche de

            std::vector<UnType> readFile(std::string const & filename){
                std::ifstream ifs(filename);
                if(! ifs){
                    throw std::runtime_error("unable to open file");
                }
                /* arrivé ici, le fichier est accessible, c'est déjà
                 * "pas mal, hein"
                 * on va maintenant essayer de lire dedans
                 */
                std::string temp;
                /* tout en remplissant un tableau de UnType */
                std::vector<UnType> tab;
                while(std::getline(ifs, temp){
                    /* Pour chaque donnée extraite à partir de temp,
                     * on doit en vérifier la validité et lancer une
                     * exception si cette vérification échoue
                     */
                    A myA;
                    /* extraction de myA depuis temp; */
                    if(! isValid(myA) ){
                        throw std::runtime_error("invalid A detected");
                    }
                   B myB;
                    /* extraction de myB depuis temp; */
                    if(! isValid(myB) ){
                        throw std::runtime_error("invalid B detected");
                    }
                    /* ... */
                    
                   Z myZ;
                    /* extraction de myZ depuis temp; */
                    if(! isValid(myZ) ){
                        throw std::runtime_error("invalid Z detected");
                    }
                    tab.emplace_back({myA,myB/*, ... */, myZ} );
            
                }
            }

            Maintenant, nous pouvons placer la post condition "finale": notre tableau ne peut pas être vide (ou doit contenir minimum XXX éléments, ou doit en contenir précisément YYY ou ????).

            Et nous en revenons toujours au même point, à savoir que:

            une même cause (une post condition n'est pas remplie et nous avons été dans l'incapacité d'y apporter une solution correcte) aura toujours les mêmes effets (il est donc préférable de laisser planter l'application plutôt que de courir le risque de la laisser fonctionner dans un "état inconsistant" )

            Nous terminerons donc le développement de la fontion readFile en lui donnant une forme finale proche de

            std::vector<UnType> readFile(std::string const & filename){
                std::ifstream ifs(filename);
                if(! ifs){
                    throw std::runtime_error("unable to open file");
                }
                /* arrivé ici, le fichier est accessible, c'est déjà
                 * "pas si mal", hein?
                 * on va maintenant essayer de lire dedans
                 */
                std::string temp;
                /* tout en remplissant un tableau de UnType */
                std::vector<UnType> tab;
                while(std::getline(ifs, temp){
                    /* Pour chaque donnée extraite à partir de temp,
                     * on doit en vérifier la validité et lancer une
                     * exception si cette vérification échoue
                     */
                    A myA;
                    /* extraction de myA depuis temp; */
                    if(! isValid(myA) ){
                        throw std::runtime_error("invalid A detected");
                    }
                   B myB;
                    /* extraction de myB depuis temp; */
                    if(! isValid(myB) ){
                        throw std::runtime_error("invalid B detected");
                    }
                    /* ... */
                    
                   Z myZ;
                    /* extraction de myZ depuis temp; */
                    if(! isValid(myZ) ){
                        throw std::runtime_error("invalid Z detected");
                    }
                    tab.emplace_back({myA,myB/*, ... */, myZ} );
            
                }
                if(tab.empty() ) { // ou n'importe quelle condition
                                   // imposée en tant que post condition
                    throw std::runtime_error("post condition not verified");
            }
                return tab;

            L'un dans l'autre, ce code présente un aspect très "programmation défensive", dans le sens où il effectue un teste presque une ligne sur deux, mais cette logique est rendue obligatoire par:

            • l'obligation qui est donnée à la fonction de respecter "sa part du contrat" (j'ai reçu une donnée valide, je dois donc renvoyer une donnée valide)
            • le fait que l'on ne peut -- décidément -- faire aucune confiance aux "données extérieures"

            Et bien sur, la grosse différence avec la programmation défensive tient surtout dans le traitement effectué lorsque "quelque chose ne va pas":

            En programmation défensive, nous renvoyons une valeur qui devra être récupérée (et testée) par "la fonction appelante", alors que la programmation par contrat va considérer comme "tout à fait normal" de voir planter l'application si un contrat est rompu ;)

            • Partager sur Facebook
            • Partager sur Twitter
            Ce qui se conçoit bien s'énonce clairement. Et les mots pour le dire viennent aisément.Mon nouveau livre : Coder efficacement - Bonnes pratiques et erreurs  à éviter (en C++)Avant de faire ce que tu ne pourras défaire, penses à tout ce que tu ne pourras plus faire une fois que tu l'auras fait
              12 mai 2019 à 17:04:39

              Merci Koala001 pour cette réponse si longue et argumentée.

              Je note, que comme Int21, ton premier exemple est un cas d'école, et ne correspond pas au besoin que j'aurai au boulot. De plus, comme le dit Ksass'Peuk, ce devrait être les tests U qui trouvent le PB avant de mettre les sources en intégration. Dans ce cas, je me pose le question de l’intérêt d’ajouter un "assert".

              En ce qui concerne la seconde partie de ton post  ("l’événement externe"), pour moi, c'est un peu différent, car suivant ce que j'avais compris, ce n'est plus un contrat, mais la robustesse du code (En résumé, c'est gérer par des exceptions, pas des assert).

              Le point qui n'est pas encore clair pour moi, ce sont les "contrats d'invariant". Je profite de cette réponse pour vous faire part de la seule expérience que j'ai eu. Sur un projet, il a été décidé qu'une table d'élément était super/hyper  critique ! L'AQ nous a forcé à mettre pour chacun des éléments du tableau un CRC. Nous nous somme donc fait une procédure (sous mutex) qui écrivait dans le tableau l'élément, calculer le CRC et l'ajouté, ainsi une procédure (sous le même mutex) qui lisait l'élément après avoir vérifier le CRC. A la réflection, ce CRC ne servait à rien, car on utilisait toujours ces "handlers" d'écriture et de lecture, alors pourquoi le CRC serait-il mauvais ?

              Tout ça pour vous dire que je ne sais pas si je saurais trouvé des "contrat d'invariant" utile et efficace.

              Merci encore pour le temps que vous avez consacré à ma répondre.

              Bien cordialement.

              • Partager sur Facebook
              • Partager sur Twitter
                12 mai 2019 à 19:56:43

                Dedeun a écrit:

                Dans ce cas, je me pose le question de l’intérêt d’ajouter un "assert".

                Pour les postcondition, l'utilisation sera toujours limité parce que tu ne pourras généralement tester qu'une partie de tes postconditions à moins payer un très gros surcoût. De fait, tu ne pourras vérifier la plupart des postconditions intéressantes qu'à l'aide de tests ou de preuve externes à la fonction. Exemple très simple : une fonction "search and replace". Pour mettre un assert de postcondition qui soit capable de contrôler toute la propriété fonctionnelle, tu dois sauvegarder l'état d'origine du tableau. Mais tu peux contrôler une partie des propriétés, typiquement si l'élément à remplacer est différent de l'élément remplaçant, alors l'élément remplacé ne doit plus être présent dans le tableau.

                Et là c'est un exemple très simple où le coût serait déjà élevé. Dans la réalité il y a un paquet de postconditions qui ne peuvent pas être testées à l'aide d'assertions sans que ça implique un temps de calcul dément. Typiquement : la postcondition d'une fonction de tri est d'avoir une permutation triée du tableau d'origine. Bon courage pour mettre un assert efficace pour "est une permutation de".

                Dedeun a écrit:

                En ce qui concerne la seconde partie de ton post  ("l’événement externe"), pour moi, c'est un peu différent, car suivant ce que j'avais compris, ce n'est plus un contrat, mais la robustesse du code (En résumé, c'est gérer par des exceptions, pas des assert).

                Pour les événements externes, on fera généralement appel à une classe de postcondition spécifique qui à chaque type d'exception va associer un état respecté par les objets mis en jeu dans le programme. Mais si, on peut tout à fait spécifier des choses à ce sujet (à noter qu'à nouveau, on restera quand même limité par l'overhead mémoire et calculatoire sur ce qu'on peut vérifier à runtime).

                Dedeun a écrit:

                Le point qui n'est pas encore clair pour moi, ce sont les "contrats d'invariant". Je profite de cette réponse pour vous faire part de la seule expérience que j'ai eu. [...]

                Tout ça pour vous dire que je ne sais pas si je saurais trouvé des "contrat d'invariant" utile et efficace.

                Il est rare qu'un objet ne vérifie pas d'invariant pour garantir sa correction. L'exemple typique c'est le fait que les structures sous jacentes doivent être allouées. Après, tu peux avoir des dépendances de valeurs entre les données entre les différents composants de la classe (exemple typique : la capacité d'un vector est supérieure ou égale à sa taille), etc. Cependant, plus l'invariant est élaboré plus il va devenir difficile (voir impossible), de le vérifier au runtime sans faire exploser le temps de calcul.

                -
                Edité par Ksass`Peuk 13 mai 2019 à 9:01:00

                • Partager sur Facebook
                • Partager sur Twitter

                Posez vos questions ou discutez informatique, sur le Discord NaN | Tuto : Preuve de programmes C

                  12 mai 2019 à 22:03:22

                  Merci pour cette nouvelle réponse Ksass`Peuk.

                  Je vais y réfléchir ... Je me permettrai de revenir sur ce point quand j'aurais les idées plus claires.

                  Merci encore.

                  • Partager sur Facebook
                  • Partager sur Twitter

                  [metho] Post condition/Invariant

                  × Après avoir cliqué sur "Répondre" vous serez invité à vous connecter pour que votre message soit publié.
                  × Attention, ce sujet est très ancien. Le déterrer n'est pas forcément approprié. Nous te conseillons de créer un nouveau sujet pour poser ta question.
                  • Editeur
                  • Markdown