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:	[INFO:INFO_OH] Computer Science/Other ML preuve de programme programmation fonctionnelle
Online Access:	http://tel.archives-ouvertes.fr/tel-00008416 http://tel.archives-ouvertes.fr/docs/00/04/77/02/PDF/tel-00008416.pdf

id	ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-00008416
record_format	oai_dc
spelling	ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-000084162013-01-07T19:09:32Z http://tel.archives-ouvertes.fr/tel-00008416 http://tel.archives-ouvertes.fr/docs/00/04/77/02/PDF/tel-00008416.pdf Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML Baro, Sylvain [INFO:INFO_OH] Computer Science/Other ML preuve de programme programmation fonctionnelle 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. 2003-07-10 FRE PhD thesis Université Paris-Diderot - Paris VII
collection	NDLTD
language	FRE
sources	NDLTD
topic	[INFO:INFO_OH] Computer Science/Other ML preuve de programme programmation fonctionnelle
spellingShingle	[INFO:INFO_OH] Computer Science/Other ML preuve de programme programmation fonctionnelle Baro, Sylvain Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML
description	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.
author	Baro, Sylvain
author_facet	Baro, Sylvain
author_sort	Baro, Sylvain
title	Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML
title_short	Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML
title_full	Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML
title_fullStr	Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML
title_full_unstemmed	Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML
title_sort	conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ml
publisher	Université Paris-Diderot - Paris VII
publishDate	2003
url	http://tel.archives-ouvertes.fr/tel-00008416 http://tel.archives-ouvertes.fr/docs/00/04/77/02/PDF/tel-00008416.pdf
work_keys_str_mv	AT barosylvain conceptionetimplementationdunsystemedaidealaspecificationetalapreuvedeprogrammesml
_version_	1716455610308886528

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

Similar Items