Travaux dirigés/pratiques - B

Méthode formelle – Méthode B

DESS QUASSI

Novembre 2001

 

 

1         Exercice 

1.1      Spécification

Construire une machine abstraite fournissant les opérations :

  1. Une opération « maximum » qui prend 2 entiers relatifs et retourne le plus grand des deux.
  2. Une opération « sqrt » qui calcule la racine carrée d’un entier naturel fournit en entrée par approximation.
  3. Une opération « swap » qui «échange » le contenue de deux variables.
  4. Une opération « division euclidienne » qui a partir des entrées a et b calcule les sorties q et r tel que a = b*q+r

1.2      Implantation

Raffiner la machine abstraite précédente afin de l’implanter.

 

2         Exercice

Soit la machine abstraite suivante :

MACHINE

Students(max_students, STUDENT)

VARIABLES

students

INVARIANT

students <: STUDENT

& card(students) <= max_students

INITIALISATION

students := {}

OPERATIONS

Enter(s) =          /* ajoute un étudiant à l'ensemble */

PRE

...                     /* a completer */

THEN

students := students \/ {s}

END;

 

Remove(s) =   /* enlève l'étudiant de l'ensemble */

PRE

...             /* a completer */

THEN

students := students - s

END;

 

Print =              /* Affiche à l’écran tous les étudiants */

            ….

END

2.1      Première partie

  1. Corriger les erreurs
  2. Compléter les pré conditions des opérations Enter et Remove,
  3. Compléter le corps de l’opération Print.

2.2      Seconde partie

Raffiner et/ou implanter la spécification précédente.

 

3         Gestion d’une banque

On considère un système de gestion d'une banque. On veut écrire partiellement la spécification du système. On dispose de deux ensembles : Numéros des comptes des clients et numéros des clients.

 

Ecrire une machine abstraite spécifiant

 

4         Gestion d’un système informatique

Une application gère l'utilisation d'un système informatique. Pour cela, des personnes sont enregistrées comme utilisateurs de ce système. A un moment donné, certains utilisateurs sont connectés à l'ordinateur. Il n'y a pas de connexions multiples; un utilisateur est soit connecté ou déconnecté.

 

Utilisez le langage B pour spécifier formellement cette application en donnant:

·        l'état du système;

·        l'opération pour ajouter un utilisateur;

·        l'opération pour supprimer un utilisateur;

·        l'opération pour se connecter

·        l'opération pour se déconnecter.

 

Pour chacune de ces opérations, considérez les traitements d'erreur. Donnez aussi une description en langue naturelle de chaque opération.