Abstract FR:

Nous nous sommes interesse a la possibilite d'extraire automatiquement une specificqtion formelle a partir d'un programme imperatif ecrit dans un langage dedie au calcul formel. Le langage choisi est aldor. Les specifications extraites sont ecrites dans un formalisme issu de la theorie axiomatique des ensembles de zermelo. Nous avons partiellement implante cette theorie dans le prouveur coq (developpe a l'inria).