Re: pre-conditions / post-conditions / expression functions / ...

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

> 
> Le 20/04/2021 à 00:14, Thomas De Contes via Ada-france a écrit :
>> J'ai jeté un coup d'oeil au Rationale : http://www.ada-auth.org/standards/12rat/html/Rat12-1-3-2.html

>> 1 Dans l'exemple donné pour Value_Present, la post-condition est identique au corps (sauf erreur). Ça veut dire que sans
>> optimisation, on fait le même calcul 2 fois, et on constate qu'on a
>> le même résultat. Est ce que ça a un sens ?

> Oui, ça arrive souvent,
> les contrats sont parfois même plus complexes
> que le corps de la procédure, c'est la beauté des preuves formelles...
> et c'est pour ça qu'on a prévu de pouvoir les débrancher.

Est ce que si on ne débranche pas, le compilateur fait quand même "naturellement" les optimisations qui nous paraissent évidentes (pas forcément celle de Find) ?
Ou alors est ce qu'il faut compter sur le fait que ça ne soit pas fait, au motif que l'usage est de les débrancher pour la version de prod (donc pas une fonctionnalité prioritaire) ?

> 
> Il y a cependant un point fondamental qui répond à beaucoup de tes
> questions:
> En Ada, un principe fondamental est l'indépendance entre spécification
> et implémentation. On n'a pas besoin de regarder dans le corps pour
> utiliser une opération, et en fait on peut utiliser un paquetage dès
> qu'on a la spec, même si on n'a pas encore écrit le corps.

Je connaissais le principe ...

> 
> Les pré/post conditions font partie de la spécification, et c'est bien
> normal puisque c'est un contrat avec l'utilisateur. Et il faut bien
> fournir un corps, même si c'est parfois identique à la post-condition.

... Merci pour ce détail, qu'il était utile de me rappeler :-)


Mais en relisant bien tout, pour Value_Present, je serais quand même tenté de "remonter le corps dans la spec", ce qui permet notamment de la factorisation de code (toujours intéressant même en dehors des questions d'optimisation) :

function Value_Present(A: Atype; X: Integer) return Boolean is
   (for some M in A'Range => A(M) = X)
   with Post => Value_Present'Result = Value_Present(A, X);

Du coup, vu l'allure de la post-condition, elle ne me parait plus très utile :-) , donc je l'aurais supprimée.
(En plus ça doit tomber dans une boucle infinie, non ?)

Est ce qu'en me lisant, tu es tenté de dire que je n'ai rien compris au principe des contrats ?


> 
>> Dans l'exemple donné pour Find, la pre-condition n'est pas identique au corps, mais c'est quand même à peu près la même quantité de travail. Est ce qu'on compte sur le compilateur pour nous faire une /grosse/ optimisation ?

> Ou supprimer les conditions pour la version de
> prod.

D'où l'usage de "-gnata", que j'ai compris à la suite de ca :-)

À propos, quand une bibliothèque externe qui contient des assertions dans sa partie publique est compilée sans "-gnata", et que je compile avec "-gnata" une unité qui utilise cette bibliothèque, est ce que les assertions publiques de cette bibliothèque vont être vérifiées ?


> NB: on laisse le contrôles (de sous-type par ex.) en version de prod,
> 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.
D'ailleurs, c'est bien le cas avec le test similaire sur les pointeurs (not null access), qui n'est d'ailleurs pas catégorisé comme assertion (alors que ça pourrait : il me semble bien que ça en respecte tous les critères).


Alors, pour tout activer tout le temps c'est assez facile, il suffit d'avoir un peu de rigueur et de mettre "pragma Assertion_Policy (Check);" partout où c'est nécessaire (dans chaque paquetage ?).

Mais ça entraine 2 questions :


1)
Est ce que ça donne un mécanisme de vérification suffisamment robuste pour qu'on puisse, en toute tranquillité, à la fois :
- dans le corps du sous-programme, considérer que les pré-conditions sont forcément respectées, donc pas besoin de les tester à nouveau,
- au moment d'utiliser le sous-programme, prévoir un traitement d'exceptions pour traiter le cas où les pré-conditions ne sont pas respectées, sans avoir besoin de les tester avant l'appel du sous-programme ?

Ou bien est ce qu'on est censé toujours considérer que les assertions sont facultatives et doivent être toujours vraies,
et on doit donc, surtout si le fonctionnement du programme en dépend, répéter le test des pré-conditions dans le corps des sous-programmes ?
(Dans ce cas là c'est dommage, ça reste très intéressant quand même, mais ça perd de son potentiel.)


2)
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à ?

- Je vois bien comment sélectionner la catégorie d'assertions.
- 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.
- 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.)



> 
>>> Readers are invited to discuss whether the A is upside down and the
>>> E backwards or whether they are both simply rotated.
>> :-D
> Humour de Barnes typique...

Blasé ? :-)



> 
>> Je devine que c'est recommandé de simplifier les fonctions en "expression functions", dans le corps du paquetage, des que c'est possible, comme pour toutes les simplifications qui améliorent la lisibilité. Mais est ce qu'on doit les faire passer dans la spécification du paquetage des que c'est possible ? Ça je n'en suis pas sur.

> Le but premier des "fonctions-expressions" est de donner un
> nom à une
> sous-expression, comme on fait en maths:
> Delta=B**2-4AC
> 
> L'autre point imporant est qu'elles peuvent apparaître en spec.
> Dans la mesure ou autrement on écrirait la même expression de façon
> moins lisible, ce n'est pas une "révélation" de l'implémentation.

(Je ne suis pas sur de bien comprendre la dernière phrase.)

Est ce que les fonctions-expressions ont le statut de spec ou de corps selon le contexte ?
Ou bien est ce qu'elles ont toujours le statut de corps, même placées dans la spec du paquetage, avec une spec implicite selon le même principe que les fonctions qu'on ne met pas dans la spec du paquetage ?

> 
> Autre principe fondamental: on en met le moins possible dans la spec,
> "tout ce qui est dans la spec pourra être retenu contre vous". Il n'y a
> donc aucune raison de "remonter" une fonction-expression dans la spec si
> ce n'est pas nécessaire à l'interface.
> 
>> Le Rationale explique clairement que c'est plus lisible de mettre
>> dans la spécification du paquetage les "expression functions" qui
>> servent dans les pre-conditions / post-conditions.
> Cela permet qu'aucune partie du contrat ne soit cachée. Si on utilise des fonctions normales, l'utilisateur ne sait pas (à part la doc) ce qu'elles font.

J'ai bien compris cette partie :-)

> 
>> J'imagine que
>> c'est pareil pour des choses similaires comme les invariants, des que
>> ça se trouve dans la spécification du paquetage. Est ce que c'est
>> tout, et dans tous les autres cas il vaut mieux que le corps de la
>> fonction reste dans le corps du paquetage ?
> D'une façon générale:
> 1) On ne met dans la partie visible que ce qui constitue strictement l'interface
> 2) On met en partie privée les déclarations privées qui résultent de la partie visible, plus éventuellement d'autres déclarations directement ou indirectement nécessaires à la complétion des types privés.
> 3) On met tout le reste dans le corps.

J'ai bien compris le principe selon lequel, quand on a plusieurs choix, le meilleur est le plus simple (décliné pour la spécification sous la forme "on pousse dans le corps"). :-)

En ce moment j'ai des problèmes d'ordre d'élaboration.
Que dis-tu du cas où une fonction-expression ne sert pour aucune assertion, mais pour initialiser une constante publique ? Est ce que la légitimité est la même ?

Si j'ai un petit paquetage dans lequel je n'ai que des fonctions simplifiables en fonctions-expressions, je serai tenté de tout mettre dans la spec pour économiser un fichier.
Est ce que c'est juste une très mauvaise idée,
ou est ce que c'est acceptable de mettre le corps des fonctions-expressions en partie privée de la spec, du fait que ça fait quand même une séparation avec la partie visible, et que ça respecte les règles de visibilité ?



> 
> 
>> Ca m'a conduit à l'Ada Reference Manual : http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-6-1-1.html
>> 3 l 3/3 : La définition de Post'Class n'est pas symétrique à celle de
>> Pre'Class : est ce que c'est simplement une erreur, ou y a t il
>> quelque chose à comprendre ?
> C'est une conséquence du LSP (Liskov Substitution Principle). Une pré-condition est l'intersection de toutes les conditions possibles de la hiérarchie; une post-condition est l'union de toutes les conditions.
> 
> Voir l'abondante littérature sur le LSP, c'est loin d'être évident a priori (il y a eu de longues discussions à l'ARG avant qu'on se mette d'accord).

Ah bon alors je ne vais pas me plonger là dedans immédiatement :-)
Je tacherai de me souvenir de ta réponse si j'en ai besoin plus tard, pour la relire.

(C'est déjà arrivé avec des trucs que tu m'as écrit il y a 20 ans ;-) - Ça ne nous rajeunis pas :-D )

> 
>> l 18.2/4 : Il me semble qu'il manque un point, au début.
> Je ne pense pas. Le paragraphe est décalé vers la gauche à cause de la longueur du numéro, mais ce n'est pas un item du "as follows" d'avant.

Ah, ok.

(C'est trop ardu pour que je puisse comprendre tout ce que je lis "comme ça".
Ce qui m'a fait pensé à une erreur, c'est que :
- on a 2 compléments à la ligne 18 qui ont été ajoutés en même temps (il me semble que c'est ça que veut dire le "/4" sur les 2 lignes),
- on a une liste à 1 élément (18/4 et 18.1/4) (il me semble que ça n'est pas courant, dans ce genre de document ?),
- 18.2/4 fait référence à "subprogram S".)

> 
>> 4 l 9/3 : Pourquoi les procédures nulles n'ont pas le droit d'avoir
>> des pre-conditions / post-conditions ? Par exemple ça aurais permis
>> de simplifier un peu l'implémentation de Ada.Assertions.Assert. Pas
>> indispensable, mais je ne vois pas l'intérêt d'avoir fait une
>> exception pour ce cas de figure.
> ??? Une pré-condition est une exigence requise de l'appelant pour que la procédure fonctionne correctement, une post-condition est une garantie sur ce que fournit la procédure. Une procédure qui ne fait rien ne peut avoir ni exigences, ni promesses...

C'est vrai que Ada.Assertions.Assert est probablement le seul cas où ça aurais pu avoir une quelconque utilité (quoi que).

Mais je trouve ça bête d'avoir prévu un cas particulier pour les procédures nulles.
Pour moi c'est un peu comme si, pour "for all", on avait prévu un cas particulier pour l'intervalle vide, pour que ça réponde ce qui est logique pour le "bon sens populaire" plutôt que ce qui est logique en math-info.

> 
>> 5 À l'intersection des "expression functions" et des procédures
>> nulles : Les procédures "unitaires" (?)
>> C'est à dire les procédures dont le corps est constitué d'exactement
>> 1 appel d'une autre procédure. Les paramètres peuvent être des
>> expressions d'une complexité quelconque, sur le modèle du corps des
>> "expression functions".
>> Est ce que ça a été proposé pour la norme 202x ? Pas suffisamment
>> utile ? Il me semble que ça contribuerais à améliorer la lisibilité,
>> même en restant dans le corps des paquetages.
> 
> Non, mais il existe une règle AdaControl pour les repérer

Je n'ai pas compris ta réponse :

- "Non" ça veut dire "pas proposé pour la norme 202x" ou "ça n'améliorerais pas la lisibilité" ?

- Que penses tu de ma suggestion ? Utile ou pas ?

- Ça sert à quoi de les repérer ?
Puisqu'on ne peut pas simplifier le code comme avec les fonctions-expressions.
(Peut-être peut on le simplifier autrement ?)


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