Re: J'aimerais

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.

Je comprends ce n'est pas tellement un problème de header ou de les compiler mais plus du système de type des langages.

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

Je n'ai (malheureusement) jamais touché à ADA., mais les énumérations de Java m'ont l'air d'avoir les même caractéristiques. Et je trouve en effet que c'est de loin bien meilleur que ce que propose le C++.

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

Les choses comme JML ou ce qui semble être ajouté à ADA 2012 m'ont l'air nettement plus pertinent que de ce limiter à un système de type. Par exemple

// je crois que ce genre de condition sont possibles
/*@ requires i > j; @*/
public void foo(int i, int j) {
 // ma méthode
}

C'est à, mon avis, l'un des points forts de D : http://www.d-programming-language.org/cppdbc.html

Mais c'est quelque chose de complémentaire au type.

Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)