SEANCE 1


1) Login sur ensisun 
===================

Nom de machine : ensisun
nom de login : le nom de famille suivi de la premiere lettre du prenom
	       le tout en minuscule
	       
Mot de passe initial : AtB06UFR


Lancez le script suivant :            ~stoulsn/EXOS_ATELIERB/PremiereConnection.sh
Puis prenez en compte les modifs :    source .bashrc
Commande de lancement de l'outil :    lanceAB &

Les TP sont dans le repertoire ~stoulsn/EXOS_ATELIERB


2) Premier TP
=============



 1 - Recopier le repertoire ~stoulsn/EXOS_ATELIERB/EXEMPLE_COURS
  ( cp -R ~stoulsn/EXOS_ATELIERB/EXEMPLE_COURS ~/. )


 2 - Lancer l'outil 
  ( lanceAB & )
  
 3 - creer un projet
  ( Attach
      -> Nom de projet : <VotreLogin>-Exemple1 
         (!!! METTEZ BIEN VOTRE LOGIN DANS LE NOM DU PROJET !!!)
      -> Database Directory : .../EXEMPLE_COURS/bdp
      -> Translation Directory : .../EXEMPLE_COURS/lang )


 4 - Ajouter les librairires nécessaires
   (Sélectionnez le projet créé 
     -> Libraries...
        -> add
           -> Library)

 5 - entrer dans le projet 
   ( double clique ou OPEN)
  
 6 - charger dans l'outil les specifications WP_EXEMPLE et WP_R1_EXEMPLE
  ( Components
      -> add ../src/WP_EXEMPLE
      -> add ../src/WP_R1_EXEMPLE)


 7 - faire le type-check

 8 - generer les obligations de preuve  
  ( POGenerate 
      -> Full)


 9 - tenter de résoudre les preuves en automatique force 0 ou 1
  ( Prove 
      -> Force 0
     ou
      -> Force 1)

10 - Regarder les obligations de preuve non résolues et comprendre a quoi elles correspondent 
  ( Analysing 
      -> Show/Print PO
        -> Choix d'une operation
           -> Display => Mode ASCII
          ou
           -> Pretty Print + OK => Mode mathematique )

   Note : la notation R<+Q est définie par : 
          {(x|->y) | ((x/:dom(Q)) & (x|->y):R) or (x|->y : Q)}



11 - Trouver celles qui ne sont pas prouvables. 
      => Donner les conditions necessaires en ajoutant une condition IF THEN ELSE.


12 - Re-faire les preuves en automatique force 0 ou 1
  ( Prove 
      -> Force 0
     ou
      -> Force 1)





3) FAIRE le TP DIVISION
=========================

Recopier le repertoire DIVISION

ouvrir un projet DIVISION
ajouter la librairie de base
aller dans le projet DIVISION
charger les specifications
regarder les obligations de preuve
produire le code a partir de MachineDeTest_imp






4) FAIRE LE TP RECHERCHE
========================


Recopier le repertoire RECHERCHE

Le fichier src/recherche2.imp contient une opération IndiceVal 
dont le comportement est décrit dans le fichier src/recherche.mch.
Nous voulons décrire le corps de cette opération. Pour cela nous 
utilisons une boucle et 3 variables locales : trouve, IndexCour et tmp.

Complètez cette opération et vérifiez la correction de votre 
proposition par la preuve. 


Si certaines obligations de preuves ne peuvent etre résolues automatiquement, 
alors imprimez les et expliquez de manière détaillée comment les prouver.