Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML

Pouvoir vérifier la conformité d'un programme avec sa spécification représente un enjeu important. On peut utiliser un assistant de preuve : un logiciel permettant la description du problème, la construction des preuves et leur vérification. Nous avons implémenté un système où l'utilisateu...

Full description

Bibliographic Details
Main Author: Baro, Sylvain
Language:FRE
Published: Université Paris-Diderot - Paris VII 2003
Subjects:
ML
Online Access:http://tel.archives-ouvertes.fr/tel-00008416
http://tel.archives-ouvertes.fr/docs/00/04/77/02/PDF/tel-00008416.pdf