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

Bonjour :-)


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 ?

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 ?


> Readers are invited to discuss whether the A is upside down and the E backwards or whether they are both simply rotated.

:-D


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



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 ?

l 18.2/4 :
Il me semble qu'il manque un point, au début.


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.


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.



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