Le problème est que le contrat est runtime et nécessite un test pour s’exercer. Il n'est pas possible d'avoir des contrats compile-time ou de vérifier leur cohérence entre eux ?
Il y a le même problème en Ada 2012 où les contrats sont effectivement là pour générer des assertions (cf. le wikibook) et donc seulement à l'exécution. Heureusement, cela est débrayable lors de la livraison au moyen d'une pragma.
Par contre, ces mêmes contrats sont la base de la programmation en Spark (pas le truc Apache, hein !) et sont, dans ce cas, traduits en langage intermédiaire, le Why3 (avec du Ocaml dedans), pour être ensuite passés aux moteurs de preuves
[^] # Re: Le cerveau n'est pas logique
Posté par Blackknight (site web personnel, Mastodon) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Il y a le même problème en Ada 2012 où les contrats sont effectivement là pour générer des assertions (cf. le wikibook) et donc seulement à l'exécution. Heureusement, cela est débrayable lors de la livraison au moyen d'une pragma.
Par contre, ces mêmes contrats sont la base de la programmation en Spark (pas le truc Apache, hein !) et sont, dans ce cas, traduits en langage intermédiaire, le Why3 (avec du Ocaml dedans), pour être ensuite passés aux moteurs de preuves