Re: pré/post-conditions - prédicats de sous-type

Le 22 sept. 2021 à 17:50, Thomas De Contes via Ada-france a écrit :

> 
> Le 20 avr. 2021 à 10:26, Jean-Pierre Rosen via Ada-france a écrit :
> 

>> NB: on laisse le contrôles (de sous-type par ex.) en version de prod,

"par exemple" ?
Dans 11.4.2 l 10, ça parle des prédicats de sous-type, et je n'ai rien vu d'autre. Y a-t-il autre chose que j'ai raté ?



>> car on estime que le surcoût des vérifs est faible devant le gain de
>> sécurité. Ca ne s'applique plus aux contrats, qui sont souvent très
>> coûteux. Encore une histoire de compromis bénéfice/risque...
> 
> Plutôt bénéfice/coût, où bénéfice = risque évité, mais j'ai compris :-)
> 
> 
> Par contre, il y a aussi beaucoup de contrats minuscules (du genre "la chaine ne doit pas être vide", "l'entier ne doit pas être à 0", ...)
> 
> Personnellement, il me semblerait judicieux que ce type de contrat soit activé tout le temps.


Dans la plupart des cas,
la solution est évidente : les prédicats de sous-type, bien sur !

(Désolé, je ne l'ai pas vu au moment de ce précédent message alors que je l'avais sous les yeux ... probablement parce que je n'avais survolé que les pré/post-conditions à la fac - là il ne me restera plus que les invariants de type à explorer :-) )


Sauf que dans quelques cas, ça ne marche pas,
puisqu'il faut que la pré-condition et la post-condition soient identiques, pour qu'on puisse les remplacer par un prédicat de sous-type.

En reprenant l'exemple donné dans 3.2.4, on aurais :

package Ada.Text_IO is

   procedure Open   (File : in out File_Type;
                     Mode : in File_Mode;
                     Name : in String;
                     Form : in String := "")
      with Pre  => File not in Open_File_Type,
           Post => File in Open_File_Type;

   procedure Close  (File : in out File_Type);
      with Pre  => File in Open_File_Type,
           Post => File not in Open_File_Type;

Y a-t-il une solution pour ça ?



Si non, voici ma suggestion :


> Puisqu'il y a des contrats très coûteux,
> est il possible de les désactiver un par un, en se ré-alignant sur la présence de "-gnata" pour ceux là ?

(Est-ce que vous ne l'avez pas fait en considérant que les prédicats de sous-type sont suffisants ?)


> - Je ne vois pas comment sélectionner un élément comme un sous-programme, il me semble que ça s'applique à tout le paquetage à la fois.

Ajouter un argument optionnel à "pragma Assertion_Policy", pour designer l'entité dont on veut modifier la politique d'assertions, comme "pragma Unreferenced" ou "pragma Obsolescent".
(Ce sont des pragma de GNAT, je ne sais pas s'il y en a des comme ça dans le langage, je n'en connais pas beaucoup.)

> - Je ne vois pas comment choisir à nouveau de s'aligner sur la présence de "-gnata", je ne vois que la possibilité d'activer ou de désactiver complètement. (D'ailleurs, quand est-ce utile de désactiver complètement ? Je ne vois pas.)

Ajouter un élément à "policy_identifier" (11.4.2 l 9), par exemple "Default", pour revenir à la politique d'assertions par défaut (11.4.2 l 10.4).


-- 
RAPID maintainer
http://savannah.nongnu.org/projects/rapid/

_______________________________________________
Ada-france mailing list
[email protected]
https://mail.ada-france.org/cgi-bin/mailman/listinfo/ada-france