La plateforme Why n'est plus développée. Notre effort
s'est porté vers le développement de Why3.
Why est toujours maintenu, en particulier pour fournir le plug-in Jessie
de Frama-C et l'outil Krakatoa pour Java. Merci de consulter la page spécifique à Krakatoa et Jessie pour plus de détails.
Nous invitons les autres utilisateurs de Why à migrer vers Why3.
Un petit guide de migration est
fourni. Se rapporter à la documentation de Why3 pour plus de détails.
Why
Why est une plateforme de vérification de programmes.
Cette plateforme contient plusieurs outils :
- un générateur d'obligations de preuve (VCG), Why, utilisé notamment
comme composant dans les outils ci-dessous, mais pouvant être
également utilisé pour vérifier des programmes (voir ces exemples) ;
- l'outil Krakatoa de vérification de programmes Java ;
- l'outil Caduceus de vérification de programmes C ; ce dernier
est cependant avantageusement remplacé aujourd'hui par l'outil Frama-C.
L'un des points forts de la plateforme Why est son intégration de nombreux
pouveurs existants, comme les asistants de preuve Coq,
PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar, et les
démonstrateurs automatiques Simplify, Alt-Ergo, Yices, Z3,
CVC3, etc.
Documentation
Manuel utilisateur, au format
PostScript et
HTML (en anglais).
Introduction à l'outil Why donnée à l'école d'été
TYPES Summer School
2007 :
transparents
;
notes
de cours
;
exercices.
Des exemples de programmes certifiés avec Why sont rassemblés
sur cette page.
L'outil Why est présenté dans cet article.
Le support théorique de cet outil est décrit dans cette thèse.
Distribution
Why est distribué librement, sous la licence GNU LIBRARY GENERAL PUBLIC LICENSE (avec une
exception ; cf le fichier LICENSE inclus dans la distribution).
Il est disponible sous forme de :
Voici les derniers changements.
Vous pouvez récupérer des versions antérieures en accédant directement à la zone FTP.
Accès anonyme à la version de développement :
svn --username guest co https://www.lri.fr/svn/demons/why2/trunk/
Pré-requis:
- pour compiler les sources il faut OCaml 3.09 (ou supérieur)
- pour compiler l'interface graphique gwhy (optionnelle mais
hautement recommandée) il faut installer également la bibliothèque Lablgtk2 library (il existe un paquet Debian, liblablgtk2-ocaml-dev).
- aucun prouveur n'est livré avec Why, vous devez obligatoirement installer au moins un prouveur supporté de la liste ci-dessous
- pour utiliser Why avec Coq il faut au minimum Coq
version 7.4
Il existe un
Plugin
Eclipse
pour Why/Caduceus/Krakatoa.
To download/install theorem provers, look at the Prover Tips page
SMT-lib benchmarks
Un ensemble de benchmarks SMT-lib tirés de nos outils :
Why Benchmarks.
Outils connexes
For back-end provers, please look at the Prover Tips page
Contact
Il y a une liste de
diffusion pour Why où sont faites notamment les annonces de
nouvelles distributions.
Les bugs doivent être signalés en utilisant lesystème
de rapport de bugs.
Pour soumettre un bug, il faut d'abord créer un compte, en mentionnant
"Toccata" dans le champ "INRIA Research Project you work with or work in".
Crédits
- Les développeurs principaux de Why sont
Jean-Christophe
Filliâtre,
Claude Marché,
Yannick Moy,
Thierry Hubert,
Nicolas Rousset
- Ont également apporté leurs contributions au développement
:
Romain Bardou, Jean-François Couchot, Mehdi Dogguy, Christine Paulin, Yann Régis-Gianas, Xavier Urbain
- Yasuhiko Minamide a ajouté le support pour
Isabelle/HOL
- Seungkeol Choe a ajouté le support pour
HOL 4
- Des remarques et critiques constructives ont été apportées par
M. Levy, N. Magaud, C. Paulin, S. Ranise, L. Théry,
X. Urbain, F. Wiedijk, S. Boldo, G. Melquiond, ... (sorry for the ones we forget to mention)
- Michel
Levy et César Muñoz ont contribués à la bibliothèque PVS de Why
