Return to search

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'utilisateur décrit la spécification du programme dans un formalisme logique ad hoc, donne le programme dans le sous-ensemble fonctionnel de ML (comprenant filtrage, définitions récursives et fonctions partielles), puis construit interactivement les preuves de correction nécessaires pour prouver la validité du programme.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00008416
Date10 July 2003
CreatorsBaro, Sylvain
PublisherUniversité Paris-Diderot - Paris VII
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0017 seconds