To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 12/04/07 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Jeudi 12 avril, 10h30 ----------------- Yann Régis-Gianas ----------------- INRIA ======================================= Mise en pratique de la logique de Hoare pour les programmes fonctionnels purs ======================================= La programmation fonctionnelle pure a su tirer partie d'une restriction, celle d'interdire les effets de bord, pour gagner en déclarativité et en abstraction. En effet, l'absence d'un état interne semble faciliter le raisonnement sur le comportement d'un morceau de code. Il est souvent très simple de donner un sens mathématique à un programme fonctionnel et cette compréhension permet d'en saisir la structure (à travers les types algébriques), la généralité (à travers le polymorphisme et les fonctions d'ordre supérieur) et le niveau d'abstraction (à travers la modularité et les types abstraits). Malgré ces bonnes propriétés, la certification des logiciels s'est traditionnellement intéressée à la preuve de programmes impératifs en utilisant la logique de Hoare. Pour intégrer les triplets de Hoare à un langage de programmation, on annote le programme par des assertions logiques (précondition et postcondition) et on engendre des obligations de preuve. Ce modèle est efficace puisqu'il permet l'utilisation de prouveurs externes pour les décharger. Néanmoins, la présence d'une mémoire modifiable induit des complications (propriétés de séparation, de non-aliasing, du modèle mémoire) qui crée un fossé entre les propriétés qu'a en tête le programmeur et les obligations de preuve effectivement générées. Lorsqu'une preuve échoue, il est alors difficile de comprendre pourquoi le programme est incorrect. Dans cet exposé, je vous présenterai un langage fonctionnel pur très simple qui intègre des assertions logiques et utilise Coq ou Ergo pour décharger ses obligations de preuve. Nous verrons quelles ont été les adaptations nécessaires de la logique de Hoare pour intégrer les idiomes de la programmation fonctionnelle. Enfin, je vous ferai une démonstration d'un prototype.