Ici, dans la recherche en langage de programmation, ils cherchent à encoder pas mal de choses dans les types. Ils ne seraient pas fâchés que par exemple on puisse coder ces règles métier dans les types, je pense. C’est un peu différent dans l’approche mais la méthode B permet d’en spécifier formellement dans l’invariant. Le truc pour ne pas avoir l’impression d’écrire plusieurs fois la même chose, c’est que la spec soit déclarative et de plus haut niveau que le code. Genre que la sortie d’une fonction qui a la propriété de trier c’est que chaque élément est inférieur au suivant. Ça te laisse complètement le choix de la manière de trier et ça va t’engueuler si t’as commenté l’appel au tri par erreur.
Si tu écris du code qui respectent pas ces règles encodées, l’objectif c’est que ça ne compile pas. Si tu écris deux règles qui sont incompatible l’une avec l’autre, logiquement, l’objectif est que ça te dise « t’es bien mignon mais c’est impossible de maintenir la propriété que la somme des surface est la somme de l’immeuble si tu modifie pas la taille de l’immeuble quand tu modifie la taille d’un appart » et que ça compile pas, itou. Ou alors que le département vente et le département fabrication utilisent pas la même notion de surface et que donc, les règles sont incohérentes et qu’il faut préciser le modèle.
Mais garde à l’esprit que c’est de la recherche en programmation qu’on parle ici. Il s’agit pas forcément d’avoir des choses utilisables dans la seconde.
[^] # Re: Le cerveau n'est pas logique
Posté par thoasm . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Ici, dans la recherche en langage de programmation, ils cherchent à encoder pas mal de choses dans les types. Ils ne seraient pas fâchés que par exemple on puisse coder ces règles métier dans les types, je pense. C’est un peu différent dans l’approche mais la méthode B permet d’en spécifier formellement dans l’invariant. Le truc pour ne pas avoir l’impression d’écrire plusieurs fois la même chose, c’est que la spec soit déclarative et de plus haut niveau que le code. Genre que la sortie d’une fonction qui a la propriété de trier c’est que chaque élément est inférieur au suivant. Ça te laisse complètement le choix de la manière de trier et ça va t’engueuler si t’as commenté l’appel au tri par erreur.
Si tu écris du code qui respectent pas ces règles encodées, l’objectif c’est que ça ne compile pas. Si tu écris deux règles qui sont incompatible l’une avec l’autre, logiquement, l’objectif est que ça te dise « t’es bien mignon mais c’est impossible de maintenir la propriété que la somme des surface est la somme de l’immeuble si tu modifie pas la taille de l’immeuble quand tu modifie la taille d’un appart » et que ça compile pas, itou. Ou alors que le département vente et le département fabrication utilisent pas la même notion de surface et que donc, les règles sont incohérentes et qu’il faut préciser le modèle.
Mais garde à l’esprit que c’est de la recherche en programmation qu’on parle ici. Il s’agit pas forcément d’avoir des choses utilisables dans la seconde.