From types to logical assertions : automatic or assisted proofs of property about functional programs

Yann Régis-Gianas 1
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Résumé : Cette thèse étudie deux approches fondées sur l’analyse statique pour augmenter la sûreté de fonctionnement et la correction des programmes informatiques. La première approche est le typage qui permet de prouver automatiquement qu’un programme s’évalue sans échouer. Le langage fonctionnel ML possède un système de type très riche et un algorithme effectuant une synthèse automatique de ces types. On s’intéresse à l’adaptation de cet algorithme aux types algébriques généralisés (GADT), une forme restreinte des inductifs de Coq, qui ont été introduits par Hongwei Xi en 2003. Dans ce cadre, le calcul efficace d’un type plus général est impossible. On propose une stratification qui maintient les caractéristiques habituelles sur le fragment ML et qui isole le traitement des GADT en explicitant leur utilisation. Le langage obtenu, MLGX, nécessite des annotations de type qui alour- dissent les programmes. Une seconde strate, MLGI, offre au programmeur un mécanisme de synthèse locale, prédictible et efficace bien qu’incomplet, de la plupart de ces annotations. La première partie s’achève avec une démonstration de l’expressivité des GADT pour coder les invariants des automates à pile utilisés par l’analyse syntaxique LR. La seconde approche augmente le langage de programmation par des assertions logiques permettant d’exprimer des spécifications de complexité arbitraire dans la logique d’ordre supérieur polymorphi- quement typée. On vérifie statiquement la conformité de la sémantique du programme vis-à-vis de ces spécifications à l’aide d’une technique appelée logique de Hoare qui consiste à engendrer un ensemble d’obligations de preuves à partir d’un programme annoté. Une fois ces obligations de preuve traitées, si un programme est utilisé correctement et si il renvoie une valeur alors il est certain que celle-ci est correcte. Habituellement, cette technique est employée sur les langages impératifs. Avec un langage fonc- tionnel pur, les problèmes liés à l’état de la mémoire d’évanouissent tandis que l’ordre supérieur et le polymorphisme en posent de nouveaux. Nos choix de conceptions cherchent à maximiser les op- portunités d’utilisation de prouveurs automatiques en traduisant minutieusement les objets d’ordre supérieur en objets du premier ordre. Une implantation prototype du système en fournit une illustra- tion dans la preuve presque totalement automatique d’un module CAML d’arbres équilibrés dénotant des ensembles finis.
Type de document :
Thèse
Programming Languages [cs.PL]. Université paris diderot, 2007. English. 〈NNT : 2007PA077155〉
Liste complète des métadonnées

Littérature citée [139 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01238703
Contributeur : Yann Regis-Gianas <>
Soumis le : dimanche 6 décembre 2015 - 21:19:37
Dernière modification le : mardi 17 avril 2018 - 11:24:46
Document(s) archivé(s) le : samedi 29 avril 2017 - 05:37:11

Identifiants

  • HAL Id : tel-01238703, version 1

Collections

INRIA | PPS | USPC

Citation

Yann Régis-Gianas. From types to logical assertions : automatic or assisted proofs of property about functional programs. Programming Languages [cs.PL]. Université paris diderot, 2007. English. 〈NNT : 2007PA077155〉. 〈tel-01238703〉

Partager

Métriques

Consultations de la notice

178

Téléchargements de fichiers

118