Il y a plusieurs composants dans le projet Why3:
- un langage fonctionnel impur, WhyML, pensé pour écrire des programmes certifiés en grande partie par des prouveurs automatiques
- tout un outillage (interface de programmation et interfaces graphiques) pour envoyer des conditions de preuve exprimées dans un langage intermédiaire (en particulier celles générées par la vérification d'un programme WhyML) vers tout un tas de prouveurs automatiques différents, les faire tourner en parallèle, ramener les résultats à l'utilisateur, etc.
À ma connaissance il n'y a pas de "projet industriel" écrit en WhyML, le langage d'entrée principal de Why3—donc oui les exemples sont ce que les gens qui travaillent dessus vont faire par intérêt ou pour tester les limites de l'outil. Par contre, la deuxième partie a été réutilisée par les gens de SPARK/Ada pour vérifier statiquement une partie des contrats d'un programme Ada (et donc ne pas avoir besoin de retester ces contrats dynamiquement), et il paraît que ça marche plutôt bien.
C'est pour ça que Blackknight t'a parlé de Why3 quand tu parlais de "vérifier des contrats compile-time" : la plateforme Why3 est utilisée par une implémentation SPARK/Ada comme une plateforme de communication/collaboration entre un programme annoté avec des spécifications ou contrats et plein de solveurs automatiques pour les vérifier.
[^] # Re: Le cerveau n'est pas logique
Posté par gasche . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Il y a plusieurs composants dans le projet Why3:
- un langage fonctionnel impur, WhyML, pensé pour écrire des programmes certifiés en grande partie par des prouveurs automatiques
- tout un outillage (interface de programmation et interfaces graphiques) pour envoyer des conditions de preuve exprimées dans un langage intermédiaire (en particulier celles générées par la vérification d'un programme WhyML) vers tout un tas de prouveurs automatiques différents, les faire tourner en parallèle, ramener les résultats à l'utilisateur, etc.
À ma connaissance il n'y a pas de "projet industriel" écrit en WhyML, le langage d'entrée principal de Why3—donc oui les exemples sont ce que les gens qui travaillent dessus vont faire par intérêt ou pour tester les limites de l'outil. Par contre, la deuxième partie a été réutilisée par les gens de SPARK/Ada pour vérifier statiquement une partie des contrats d'un programme Ada (et donc ne pas avoir besoin de retester ces contrats dynamiquement), et il paraît que ça marche plutôt bien.
C'est pour ça que Blackknight t'a parlé de Why3 quand tu parlais de "vérifier des contrats compile-time" : la plateforme Why3 est utilisée par une implémentation SPARK/Ada comme une plateforme de communication/collaboration entre un programme annoté avec des spécifications ou contrats et plein de solveurs automatiques pour les vérifier.