Subject: M\'ecanisation des fonctions partielles Jour: 16/10/98 (Vendredi 16 octobre) http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ ___ / _ _ / __ __ /_ _ / / | _ __ _ / / \ / \ ___ / / | / /_ / __| / ___ /___/ __| / | __| |___ |_/ |_/ |____ / / __/ |_ |_/ |_ / |_/ / |_/ / / I N R I A - Rocquencourt, Salle de confe'rence du batiment 11 Vendredi 16 octobre, 14h00 ------------------- Catherine Dubois ------------------- (Lami, Evry) ============================================================ M\'ecanisation des fonctions partielles ============================================================ Notre \'etude se place dans le cadre de la sp\'ecification des op\'erations partielles dans un syst\`eme fond\'e sur une logique classique proposant la notion de fonctions totales, comme l'assistant de preuves Coq par exemple. Nous pr\'esentons un style d'\'ecriture o\`u les fonctions partielles sont d\'ecrites \`a l'aide de pr\'e-conditions d\'efinies inductivement. Notre m\'ethode permet de calculer le domaine d'une fonction partielle f ind\'ependamment du calcul de f. Nous \'etudions \'egalement l'influence dun tel style sur les preuves et utilisations ult\'erieures de la sp\'ecification. (Travail r\'ealis\'e en collaboration avec V\'eronique Donzeau-Gouge (Cedric,Cnam))