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

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
> 
> Et ça entraine quelques questions sur : - les pre-conditions /
> post-conditions - les "expression functions" (je ne sais pas traduire
> ça en français, désolé) - les procédures nulles et "unitaires" (?)
> 
> 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.

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.

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.

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

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

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

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


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

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

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

> 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


-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52
https://www.adalog.fr
_______________________________________________
Ada-france mailing list
[email protected]
https://mail.ada-france.org/cgi-bin/mailman/listinfo/ada-france