Version imprimable
Il me semblait que justement les contrats améliore les possibilités d'analyse statique. Un exemple simple comme celui présenté est faisable. Eclipse detecte bien des trucs du genreCitation:
Envoyé par tchize_
C'est juste qu'il faut le programmer... Pas simple...Code:
2
3
Mais plus une question de ressources et d'argent que de faisabilité.
Requires, Ensures... ça ressemble à s'y méprendre aux Code Contracts de .NET 4.0 ;)
Si ce n'est qu'ils ont choisi de se baser sur des annotations plutôt que sur des appels de méthode...
A moins que ce ne soit le Code Contracts de .NET 4.0 qui ressemble au Java Modeling Language... va savoir... :roll:Citation:
Envoyé par tomlev
En fait ma remarque relevait plus de la boutade que d'autre chose... je crois que ces termes sont à peu près universels dans le domaine de la programmation par contrat, donc ça n'a pas du être inventé par JML non plus ;)Citation:
Envoyé par pseudocode
Si je ne m'abuse, ce sont des termes qui ont été introduits par Bertrand Meyer pour le langage Eiffel.Citation:
Envoyé par tomlev
Pour résumer, quand on écrit une fonction (en Java ou en ??) qui a des paramètres, on a intérêt à se soucier de la validité de ceux-ci, si on veut éviter les bugs.
Dans la programmation par contrat (cf. B Meyer), on établit un contrat entre la fonction et le code client qui appelle la fonction : la fonction peut être écrite en supposant que ses paramètres vérifient une précondition ; en retour, elle garantit son effet par le biais d'une postcondition. Cette notion de contrat est finalement assez naturelle, si on cherche à concevoir proprement.
Par exemple, si on veut écrire une fonction qui interclasse deux tableaux triés, on écrit
- Précondition = les 2 tableaux sont triés
- Postcondition = le tableau résultat est trié et contient exactement tous les éléments des 2 tableaux
Tout le monde bénéficie des avantages de ce contrat : la fonction est plus simple à écrire car elle peut s'appuyer sur l'hypothèse formulée par la précondition ; le code client qui appelle la fonction a la garantie que la fonction a fait son travail correctement.
En Eiffel, préconditions et postconditions sont des formules du calcul des prédicats, sans quantificateur. Ces assertions font partie intégrante de l'interface de la classe.
Pour l'histoire, il faut savoir que Eiffel permet aussi d'écrire d'autres assertions comme les invariants d'itérations et ainsi de réaliser la preuve de l'itération. Pour les programmeurs soucieux d'écrire du code impeccable, c'est un vrai bonheur ....
Pour appliquer ce type de programmation dans un langage dont la définition ne prévoit pas ce mécanisme, comme Java, on peut :
- utiliser JML qui permet d'écrire des pré et post avec quantificateurs, qui fait quelques vérifications pour interdire d'écrire des assertions qui modifient l'état de l'objet, et qui génère du Java.
Malheureusement, JML n'a pas évolué et n'est compatible qu'avec Java 1.4 .... Dommage, c'était bien.
- utiliser assert pour faire de la programmation défensive ; la fonction se défend elle-même contre les mauvais paramètres. Pour prévenir le client qu'une exception peut être déclenchée, on ajoute un commentaire en langage naturel avec la balise @exception.
Pour éviter toute mauvaise surprise, le programmeur est tenu de n'utiliser dans un assert que des fonctions qui observent l'objet, mais qui, surtout, ne le modifient pas, de sorte que si on désactive les assert (option -ea de java), le programme fonctionne de la même façon. Mais, le programmeur fait ce qu'il veut, le compilateur ne vérifie rien ......
Dans un assert, on ne peut pas utiliser de quantificateur ; pour écrire une propriété vraie sur un intervalle on est obligé d'écrire une fonction booléenne qui fait le test.
On utilise rarement assert à la fin de la fonction pour vérifier son bon fonctionnement, mais on pourrait le faire pour vériier la postcondition.
Donc pour résumer, si Java doit intégrer les pré et post, ce sera une bonne chose. S'il pouvait aussi intégrer les invariants d'itérations, on ne verrait peut-être plus trainer du code Java avec 2 itérations imbriquées et un return pour en sortir ......
Il reste à former les programmeurs pour utiliser les assertions et les inciter à bannir le bricolage. Tout un programme ....:ccool:
Pour moi et d'après plusieurs lectures (sur lesquelles je ne mets plus la main), le but des assert en java est de pouvoir blinder le développement.Citation:
Envoyé par aimejeai
On les active en développement et on les désactive en production pour gagner en vitesse. Tout ce qui doit systématiquement être testé même en production (par ex des valeurs saisies par un utilisateur) ne doit pas l'être via un assert(...) mais via un if (...) throw...
En tout cas, c'est comme ça que les utilise. Sinon, je ne vois pas la différence entre des assert et des if.