C'est certain, mais dans certaines fonctions de bibliothèques les spécifications sont bien connues et c'est ce que l'on teste avec les tests unitaires. Si je reprend, par exemple, mon interface Anneau d'un commentaire précédent, on doit avoir comme propriété que add x (neg x) = zero pour tout valeur de x. Ça s'exprime et se prouve en Coq, ce qui est hors de portée des tests unitaires.
Ceci étant, la référence aux systèmes avec typage dépendant avait pour seul but de justifier la proposition : plus on enrichit le système de types, moins on a besoin de tests unitaires. Proposition implicitement soutenue par rewind qui est à l'origine de cette sous discussion dans les commentaires.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Performance
Posté par kantien . En réponse au journal Moi, expert C++, j'abandonne le C++. Évalué à 4. Dernière modification le 06 juin 2019 à 01:04.
C'est certain, mais dans certaines fonctions de bibliothèques les spécifications sont bien connues et c'est ce que l'on teste avec les tests unitaires. Si je reprend, par exemple, mon interface Anneau d'un commentaire précédent, on doit avoir comme propriété que
add x (neg x) = zeropour tout valeur dex. Ça s'exprime et se prouve en Coq, ce qui est hors de portée des tests unitaires.Ceci étant, la référence aux systèmes avec typage dépendant avait pour seul but de justifier la proposition : plus on enrichit le système de types, moins on a besoin de tests unitaires. Proposition implicitement soutenue par rewind qui est à l'origine de cette sous discussion dans les commentaires.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.