Why3 est ce qu'on appelle un générateur de conditions de vérification, c'est à dire un outil transformant un programme contenant des spécifications formelles (typiquement formulées sous la forme de pré- et post-conditions) en un ensemble de formules logiques (les dites conditions de vérification) dont la validité implique que le programme respecte sa spécification. Une fois générées, Why3 transmet ces conditions de vérification à divers outils pour essayer de démontrer leur validité automatiquement; celles pour lesquelles ce processus échoue sont traduites vers Coq pour permettre la preuve manuelle.
(Par ailleurs, l'auteur principal de Why3 est aussi un des contributeurs historiques au cœur de Coq.)
[^] # Re: Le cerveau n'est pas logique
Posté par auve . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 6.
Why3 est ce qu'on appelle un générateur de conditions de vérification, c'est à dire un outil transformant un programme contenant des spécifications formelles (typiquement formulées sous la forme de pré- et post-conditions) en un ensemble de formules logiques (les dites conditions de vérification) dont la validité implique que le programme respecte sa spécification. Une fois générées, Why3 transmet ces conditions de vérification à divers outils pour essayer de démontrer leur validité automatiquement; celles pour lesquelles ce processus échoue sont traduites vers Coq pour permettre la preuve manuelle.
(Par ailleurs, l'auteur principal de Why3 est aussi un des contributeurs historiques au cœur de Coq.)