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...
Main Author: | |
---|---|
Language: | FRE |
Published: |
Université Paris-Diderot - Paris VII
2003
|
Subjects: | |
Online Access: | http://tel.archives-ouvertes.fr/tel-00008416 http://tel.archives-ouvertes.fr/docs/00/04/77/02/PDF/tel-00008416.pdf |