Pre, Post conditions et héritage.

[Blady]

Bonjour,

Voici un exemple (lignes 4 à 21) inspiré de celui donné au chapitre 16.2
du livre "Programming in Ada 2012" :

4. procedure Pinc (X : in out Integer) with
5. Post => X = X'Old + 1;
6.
7. procedure Pinc (X : in out Integer) is
8. begin
9. X := X + 1;
10. end Pinc;
11.
12. type Apples is new Integer;
13.
14. procedure Pinc (X : in out Apples) with
15. Pre => X >= 0,
16. Post => X = X'Old + 1;
17.
18. procedure Pinc (X : in out Apples) is
19. begin
20. X := X + 1;
21. end Pinc;
22.
23. type Apples2 is new Integer;
24.
25. procedure Pinc (X : in out Apples2) with
26. Pre => X >= 0;
27.
28. procedure Pinc (X : in out Apples2) is
29. begin
30. X := X + 2;
31. end Pinc;

(code source complet en PJ)

Le type Apples hérite du type Integer et le sous-programme Pinc en ligne
14 remplace l'ancien avec l'ajout d'une pré-condition.
L'auteur indique que le sous-programme hérite de la post-condition
automatique mais la nouvelle déclaration doit la reprendre, ce qui est
fait ici.
L'auteur ajoute "So we cannot inherit an operation and change its
condition at the same time".
Pourtant avec le type Apples2, le sous-programme Pinc en ligne 25 qui ne
reprend pas la post-condition d'origine compile et s'exécute
correctement avec GNAT et il n'y a pas d'exception levée par
l'incrémentation de 2 en violation avec la post-condition.

Est-ce qu'il y a contradiction ?
Est-ce que GNAT aurait dû sortir une erreur sur la ligne 25 ?

Merci, Pascal.

[J-P. Rosen]

Le type Apples hérite du type Integer et le sous-programme Pinc en ligne
14 remplace l'ancien avec l'ajout d'une pré-condition.

Ben non, comme Pinc opère sur Integer (déclaré dans Standard), le
sous-programme n'est pas primitif et donc pas hérité. Effectivement, il
semblerait que Barnes emporté par l'élan n'ait pas fait gaffe...

[Blady]

Post by J-P. Rosen

Le type Apples hérite du type Integer et le sous-programme Pinc en ligne
14 remplace l'ancien avec l'ajout d'une pré-condition.

Ben non, comme Pinc opère sur Integer (déclaré dans Standard), le
sous-programme n'est pas primitif et donc pas hérité. Effectivement, il
semblerait que Barnes emporté par l'élan n'ait pas fait gaffe...

Alors du coup, j'ai créé un type à moi dans un paquetage pour bien avoir
Pinc primitive :

package PA2012_05_My_I is
type My_Integer is range -1000 .. 1000;
-- P391
procedure Pinc (X : in out My_Integer) with
Post => X = X'Old + 1;
end PA2012_05_My_I;

Mais là non plus pas d'exception sur l'appel de la procédure de
remplacement avec le type Apples2:

with PA2012_05_My_I;
package PA2012_05_My_A2 is
type Apples2 is new PA2012_05_My_I.My_Integer;
procedure Pinc (X : in out Apples2) with
Pre => X >= 0;
end PA2012_05_My_A2;

L'exemple de John Barnes ne fonctionne donc pas sur Integer et la
citation porte à confusion (ici les nouvelles conditions remplacent
complètement les anciennes).
Néanmoins, y a-t-il un moyen de d'avertir l'auteur simplement du
problème avec son exemple ?

Merci, Pascal.

[J-P. Rosen]

Post by Blady
L'exemple de John Barnes ne fonctionne donc pas sur Integer et la
citation porte à confusion (ici les nouvelles conditions remplacent
complètement les anciennes).
Néanmoins, y a-t-il un moyen de d'avertir l'auteur simplement du
problème avec son exemple ?

Je lui ai déjà mis un mot, il présente ses excuses au groupe pour la
confusion...

[Blady]

Post by J-P. Rosen

Post by Blady
L'exemple de John Barnes ne fonctionne donc pas sur Integer et la
citation porte à confusion (ici les nouvelles conditions remplacent
complètement les anciennes).
Néanmoins, y a-t-il un moyen de d'avertir l'auteur simplement du
problème avec son exemple ?

Je lui ai déjà mis un mot, il présente ses excuses au groupe pour la
confusion...

Merci Jean-Pierre pour le relai.
À l'occasion ne pas hésiter pour le remercier pour son livre incontournable.
Et ... qu'une version française serait la bienvenue :-)
Je continue néanmoins ma lecture ;-)
Merci encore Pascal.