Toutes les discussions que l'on voit au dessus montrent justement qu'il y a suffisamment de façon de résoudre un problème pour que ça ne soit pas figé dans le langage. Pour autant tu peux vouloir, au sein d'un programme donné, n'autoriser qu'une seule solution à fin d'améliorer la cohérence.
Où vois-tu dans mon propos que c'est figé dans le langage ? La discussion portait sur un bout de code ADA, celui-ci :
qui générera une exception à l'éxecution car, dans ce cas du variant, il n'y a pas de champ NombreThread. C'est là une problématique de typage, et d'ailleurs le compilateur semble savoir qu'il y a problème, mais la norme semble avoir préférée émettre un warning et non une erreur de compilation. D'où la question de Guillaum : « Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage ». Question à laquelle gerfaut83 a répondu : « J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code ».
D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ? ou plutôt, comment savoir qu'un bout de code plantera nécessairement avant de le lancer ? D'où mon exemple pour refuser statiquement, par contrainte de type, un arbre vide comme entrée pour une fonction plutôt que de générer une exception à l'exécution; solution qui de plus réduit l'overhead du code généré.
Dans l'exemple ci-dessus, ce n'est pas tant une impossibilité d'inférer statiquement qu'il y aura un problème, mais un choix de la norme qui considère cela comme un avertissement et non comme une erreur critique. Mais dans bien des cas, sans ajout d'informations qui ne sont pas définies par le langage, il n'est pas possible de garantir certains invariants d'un code. Ce à quoi je faisais référence, pour aborder cette problématique, était des outils d'analyse statique comme JML pour Java présenté, par exemple, dans la conférence Intégration de la vérification formelle dans les langages de programmation.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Solution à base de types variants en ADA
Posté par kantien . En réponse à la dépêche Sortie de GHC 8.0.2 et une petite histoire de typage statique. Évalué à 2.
Où vois-tu dans mon propos que c'est figé dans le langage ? La discussion portait sur un bout de code ADA, celui-ci :
qui générera une exception à l'éxecution car, dans ce cas du variant, il n'y a pas de champ
NombreThread. C'est là une problématique de typage, et d'ailleurs le compilateur semble savoir qu'il y a problème, mais la norme semble avoir préférée émettre un warning et non une erreur de compilation. D'où la question de Guillaum : « Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage ». Question à laquelle gerfaut83 a répondu : « J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code ».D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ? ou plutôt, comment savoir qu'un bout de code plantera nécessairement avant de le lancer ? D'où mon exemple pour refuser statiquement, par contrainte de type, un arbre vide comme entrée pour une fonction plutôt que de générer une exception à l'exécution; solution qui de plus réduit l'overhead du code généré.
Dans l'exemple ci-dessus, ce n'est pas tant une impossibilité d'inférer statiquement qu'il y aura un problème, mais un choix de la norme qui considère cela comme un avertissement et non comme une erreur critique. Mais dans bien des cas, sans ajout d'informations qui ne sont pas définies par le langage, il n'est pas possible de garantir certains invariants d'un code. Ce à quoi je faisais référence, pour aborder cette problématique, était des outils d'analyse statique comme JML pour Java présenté, par exemple, dans la conférence Intégration de la vérification formelle dans les langages de programmation.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.