From: daumas@lip (Marc Daumas)
To: eleves.dmi@lip, tous.lip@lip, claire@cri, huguette.ortega@imag.fr,
        jlnicola@frcpn11.in2p3.fr
Subject: Séminaire d'Informatique des Elèves [21/11]
Date: Fri, 17 Nov 1995 17:34:06 +0100



Bonjour,

Sylvain Boulmé nous présentera  Mardi 21 Novembre le premier séminaire
de l'année fait par un étudiant. J'espère que ce sera le premier d'une
longue  liste.  Sylvain   est élève  en  deuxième année  du  magistère
d'informatique de l'École.   Il nous presentera l'environnement de son
stage de première année qui s'est déroulé de juin à juillet 1995.  Les
horaires restent inchangés 13h30-14h30, amphi A.

Titre
-----

Implantation de notions algébriques en PVS.

Résumé
------

PVS signifie Prototype Verification System. On cherche avec le temps à
faire réaliser  aux ordinateurs le plus de  tâches possibles. En toute
généralité, on  ne peut pas laisser à  un  ordinateur le soin d'écrire
automatiquement une démonstration.    PVS a été  conçu pour  décharger
l'utilisateur des  parties  répétitives des  démonstrations.  À chaque
fois que le logiciel est bloqué  dans une démonstration, il demande de
l'aide à l'utilisateur qui lui indique la ou les règles à utiliser.

Cela n'est possible   que   dans   le cadre d'un     formalisme   très
strict. Nous verrons ensemble la définition  du langage de PVS, et ses
aspects attractifs. À l'aide  d'exemple empruntés à l'algèbre  de base
(groupe, anneau, idéal),     nous pourrons parcourir    l'ensemble  du
processus de définition  d'une structure  algébrique  en PVS,  de  son
instanciation et de son utilisation.

Pour  exploiter les définitions  qui lui sont fournies, PVS transforme
les  propostions à vérifier jusqu'à  ce  qu'elles se  réduisent à  des
hypothèses.   Nous verrons ensemble les   règles dont dispose PVS pour
travailler puis  sur  l'exemple des semi-groupes   la démonstration de
l'associativité d'une loi induite sur un sous-semi-groupe.

À la fin du  stage, la structure  d'anneau euclidien était entièrement
définie  en  PVS.  Cela a   permi   de vérifier  automatiquement   que
l'algorithme d'Euclide   calcule le  PGCD   de  deux nombres   ou  que
l'ensemble des polynômes sur un corps constitue un anneau.

-- 
     .    _  .       ______________________________________
     |\_|/__/|      /                                      \   
    / / \/ \  \    /    Don't let people drive you crazy    \
   /__|O||O|__ \   \ when you know it's in walking distance /
  |/_ \_/\_/ _\ |   \  ____________________________________/
  | | (____) | ||    |/
  \/\___/\__/  // ___/
  (_/         ||    
   |          ||\   Marc Daumas (Marc.Daumas@Lip.Ens-Lyon.Fr)
    \        //_/   Lab. LIP - Equipe SAAO - ENS Lyon
     \______//      46, allee d'Italie - 69364 Lyon Cedex 07
    __|| __||       Ph  : (+33) 72 72 85 49
   (____(____)      Fx  : (+33) 72 72 80 80