To: seminaire@pauillac.inria.fr From: Bruno.Barras@inria.fr Subject: SEM - INRIA : LogiCal - 14/01/03 - Paris - FR Vous pouvez maintenant vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E . ___ / _ _ / _ / / / \ / \ / / __| / |___ |_/ |_/ / |__ |_/ |_ ___ . / / ___ __ /_ _ / _/ /| /| _ __ __ _ _ / / / /_ / __| / / |/ | / \ /_ / / \ | / __| |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ I N R I A - Rocquencourt Salle de conference du Bat 11 Mardi 14 janvier, 10h30 ----------------- Dominique Cansell ----------------- LORIA ============= La Balbulette ============= Travail commun avec Jean-Raymond Abrial 1) Contexte Nous avons déposé une opération QSL dont le nom est AdHoc. Le but de cette opération est de développer une interface ``didactique'' d'un prouveur et de valider cette interface sur une étude de cas industrielle. Le prouveur est celui de l'Atelier B (développé et commercialisé par CleaSy) qui supporte la méthode B (conçue par Jean-Raymond Abrial) que nous utilisons dans cette opération pour développer des systèmes enfouis par la preuve en collaboration avec le LIEN et TDF-C2R (Metz). Ainsi, nous définirons les fonctionnalités d'un prouveur interactif ainsi que l'interface de ce prouveur pour faciliter la preuve (interactive) dans le cadre d'un développement incrémental entièrement prouvé d'un système. Notre objectif est de ``démocratiser'' l'activité de preuve interactive pour que des ingénieurs systèmes puissent développer des systèmes par la preuve. Il faut donc absolument rendre les outils de preuves accessibles en proposant des interfaces dédiées à la preuve et en proposant des schémas de preuves aux utilisateurs du prouveur. 2) Réalisation Nous avons complètement réinventé et refait l'interface du prouveur interactif de l'Atelier B. Son nom est la Balbulette car c'est une véritable calculette logique pour faire des preuves (Nous espèrons que cela ne sera pas que pour des preuves pour B). Elle a été développée sous emacs à partir de l'interface emacs de ClearSy. Elle a été conçue pour pouvoir prouver des théorèmes avec le maximum de clics souris et le minimum de déplacements (Click'n Prove). Des boutons spécifiques correspondants aux commandes de base de la preuve (lemme annexe, preuve par cas, intanciation d'hypothèse universelle, appel du prouveur de prédicats, etc) sont associés au but et aux hypothèses visibles. Ces boutons dépendent de la forme du but ou des hypothèses en question. Ils ne sont présents que si la commande correspondante peut s'effectuer sans erreur. La Balbulette est donc une sorte de calculette logique dont les boutons évoluent avec l'avancement de la preuve. Nous avons traité avec beaucoup d'attention le problème difficile du grand nombre d'hypothèses que l'on trouve généralement dans nos lemmes. Pour cela, nous avons introduit une notion de hiérarchie d'hypothèses. Le statut d'une hypothèse peut varier: il y a les hypothèses dites sélectionnées, les hypothèse non sélectionnées mais situées dans un ``cache'', les hypothèses situées dans la ``table de recherche'' (après recherche par critère), et enfin les hypothèses invisibles (mais que l'on peut rechercher par critère puis sélectionner). L'utilisateur a la possibilité de faire varier le statut d'une hypothèse au cours de la preuve: sélection, déselection, recherche, oubli, etc. Nous avons également prêté beaucoup d'attention à la présentation sur l'écran. Plusieurs idées simples nous ont guidés: minimiser les mouvements des mains et des yeux, éviter les mouvements trop brusques sur l'écran, respecter une mise en place aussi lisible que possible des formules compliquées (zooms, vision partielle, etc), mise à disposition de zones d'éditions dynamiques spécialisées, pratique et spécialisation des clics de la souris, etc. Nous n'avons certainement pas trouvé la panacée universelle en la matière mais nous pensons qu'un effort dans ce sens rend la pratique de la preuve relativement amusante. Il y aura une démo.