Abstract FR:

Nous présentons d'abord un système théorique permettant la preuve de programmes d'ordre supérieur avec etfets de bord. Ce système est constitué de trois composantes majeures. D'abord un langage de programmation avec un système à effets, avec polymorphisme d'etfets, permettant une analyse fine des effets. Ensuite, un langage de spécitication d'ordre supérieur qui contient aussi un moyen de parler des évolutions d'états. Enfin, un calcul de plus faibles préconditions, permettant d'obtenir, à partir d'un programme annoté, des obligations de preuve, c'est-à-dire des formules dont la validité implique la correction du programme. Nous présentons également deux restrictions du système initial : la première interdit l'aliasing entre régions, ce qui garantit la modularité des spécifications : la deuxième restreint chaque région à un singleton, ne contenant qu'une seule référence. Les deux restrictions permettent de simplifier les obligations générées, mais restreignent l'ensemble des programmes acceptés. Nous présentons une implantation du système théorique. Cet outil repose notamment sur des traductions des obligations de preuve vers la logique d'ordre supérieur et la logique du premier ordre. La première traduction permet notamment l'utilisation de l'assistant de preuve Coq pour valider les obligations de preuve. La traduction vers la logique du premier ordre permet, quant à elle, l'utilisation de démonstrateurs automatiques. Des programmes d'ordre supérieur, entre autres de la bibliothèque standard d'OCaml, sont prouvés correct, ainsi qu'une implémentation à base de continuations de l'algorithme de Koda-Ruskey.