Ce n'est probablement pas aussi poussé, mais je ne vois pas très bien ce qui est ajouté ou non par ADA.
L'objectif, Michel, l'objectif !! ;)
Comme le dit la page que tu fournis, l'objectif est d'accélérer la construction du projet pas de vérifier la cohérence. Je crois que j'ai déjà donné ce lien plus haut qui te donnera plus d'explications.
En C/C++ tu as déjà une vérification du type (moins forte en C qu'en C++ certes). ADA apporte des vérifications de précondition comme le spécifie JML ?
C/C++ sont déjà des langages à typage fort, Ada fournit un système de typage qui va plus loin en incluant toutes les contraintes de valeurs pour les types simples et les vérifie seul à la compilation quand c'est possible ou en levant une exception au runtime.
Petit exemple tout simple :
procedure Test is
type MonInt is range 1..5;
Titi : MonInt := 5;
begin
Titi := Titi + 1;
end Test;
J'adore le message de warning à la compilation :
fred@freddy:/tmp $ gnatmake test.adb
gcc-4.4 -c test.adb
test.adb:6:17: warning: value not in range of type "MonInt" defined at line 3
test.adb:6:17: warning: "Constraint_Error" will be raised at run time
gnatbind -x test.ali
gnatlink test.ali
gnatlink: warning: executable name "test" may conflict with shell command
Alors, c'est vrai, l'exemple est simplissime mais dans les cas plus complexes avec énormément de types définis, ce genre d'aide n'est pas négligeable. Tu trouveras tout plein d'infos là si ça t'intéresse.
Ensuite, les énumérations sont de vrais types qui s'utilisent comme tels et on ne peut pas les substituer par leur valeur numérique sans le dire explicitment. D'ailleurs, on n'est pas censé maitriser ce mapping si on ne l'a pas spécifié.
Encore une fois, plutôt que de donner un exemple ridicule, je vais te donner un lien rien qu'à toi :D
Pour finir, je me suis aussi intéressé à JML après avoir vu ce qui se faisait en Spark Ada. Spark est un peu particulier puisque c'est un sous-langage d'Ada qui est très contraignant mais qui décrit bien les invariants, les pré-conditions... Du coup, ça avait l'air tellement bien que ce sera inclus dans la révision 2012 sous la forme définie là. Mais bon, c'est une norme ISO alors ça va prendre encore un peu de temps ;)
[^] # Re: J'aimerais
Posté par Blackknight (site web personnel, Mastodon) . En réponse au journal Votre langage idéal ?. Évalué à 2.
L'objectif, Michel, l'objectif !! ;)
Comme le dit la page que tu fournis, l'objectif est d'accélérer la construction du projet pas de vérifier la cohérence. Je crois que j'ai déjà donné ce lien plus haut qui te donnera plus d'explications.
C/C++ sont déjà des langages à typage fort, Ada fournit un système de typage qui va plus loin en incluant toutes les contraintes de valeurs pour les types simples et les vérifie seul à la compilation quand c'est possible ou en levant une exception au runtime.
Petit exemple tout simple :
J'adore le message de warning à la compilation :
Alors, c'est vrai, l'exemple est simplissime mais dans les cas plus complexes avec énormément de types définis, ce genre d'aide n'est pas négligeable. Tu trouveras tout plein d'infos là si ça t'intéresse.
Ensuite, les énumérations sont de vrais types qui s'utilisent comme tels et on ne peut pas les substituer par leur valeur numérique sans le dire explicitment. D'ailleurs, on n'est pas censé maitriser ce mapping si on ne l'a pas spécifié.
Encore une fois, plutôt que de donner un exemple ridicule, je vais te donner un lien rien qu'à toi :D
Pour finir, je me suis aussi intéressé à JML après avoir vu ce qui se faisait en Spark Ada. Spark est un peu particulier puisque c'est un sous-langage d'Ada qui est très contraignant mais qui décrit bien les invariants, les pré-conditions... Du coup, ça avait l'air tellement bien que ce sera inclus dans la révision 2012 sous la forme définie là. Mais bon, c'est une norme ISO alors ça va prendre encore un peu de temps ;)