Mobile Telecom

Windows (en fait un cd avec linux+B4free+Click’N’Prove) est maintenant disponible (cf. http://b4free.com/public/installB4W.php).

2 - Première Utilisation

Cette section décrit les actions à effectuer avant la première utilisation de B4free et de la Balbulette. Cela suppose que l’installation de ces deux outils a été effectuée. La suite de cette section décrit les actions à faire sur les machines de RezUFR (qui doivent donc être adaptées si il s’agit d’une installation sur vos machines personnelles) :

1. Placez vous dans votre répertoire racine utilisateur : cd

2. Créez un répertoire qui contiendra tous vos projets B : mkdir projB

3. Notez la référence absolue désignant ce répertoire : cd projB ; pwd

(normalement quelque chose comme /auto_home/login/projB)

4. Revenez dans votre répertoire racine utilisateur : cd

5. Exécutez la procédure de configuration depuis ce répertoire : /usr/local/Click_n_Prove.V2.0/install_personal_Click_n_Prove

6. A la question : “Give the PATH of the directory where your B development are stored ?” Donnez la référence absolue notée précédemment : /auto_home/login/projB

7. Vérifiez qu’un fichier (shell) Click_n_Prove a été crée dans votre répertoire racine

8. Dorénavant le lancement de l’outil se fait à partir de votre répertoire racine en tapant : ./Click_n_Prove

3 – Découverte de l’outil

Clearsy a réalisé un tutoriel (en flash) disponible à l’adresse http://www.b4free.com/tutorial/sampleB4free.htm.

3.1 Interface

Au lancement (commande : ./Click_n_Prove), on est en présence de deux fenêtres (cf. figure) xemacs : celle de gauche est en fait un panneau de commandes constitué de boutons qui permettent en particulier de déclencher des affichages sur celle de droite. Au démarrage il y a 6 boutons dans la zone 1 (cf. figure) dont :

- [qu] pour quitter

- [hp] pour basculer du mode « normal » au mode « aide » (et vice versa)

- [ap] pour créer un nouveau projet

Le clic se fait par le bouton droit. Il est prudent de toujours quitter en passant par le bouton [qu] et non d’utiliser les croix du gestionnaire de fenêtre, ou le quitter d’xemacs !

On remarquera que lorsqu’on passe la souris sur les boutons, une information indiquant le rôle du bouton s’affiche dans la zone 3 ou 4 (celle qui est active). Le mode aide (clic sur [hp]) permet d’obtenir de l’aide sur le fonctionnement des boutons ; dans ce mode, un clic sur le bouton pour lequel on cherche une aide affiche l’aide dans la zone 2. Ce mécanisme est disponible dans tous les écrans de commande.

Les 3 autres boutons permettent de restaurer des projets B précédemment archivés.

[pic]

3.2 Création d’un projet

Un projet B regroupe l’ensemble des machines composants un projet de développement logiciel particulier (notion proche de celle de package de Java). Pour créer un projet, on clique sur [ap] et on donne un nom à son projet.

Créez un projet TP1.

Pour chaque projet créé, une nouvelle ligne avec 5 nouveaux boutons et le nom du projet est ajoutée dans la zone 1 dont :

- [rp] pour supprimer le projet

- [op] pour ouvrir le projet

Les trois autres boutons permettent de créer des archives de sauvegarde du projet dans le sous répertoire Archives (que l’on peut alors s’échanger puis restaurer avec les 3 boutons du bas).

Ouvrez votre projet TP1.

L’ouverture de votre projet modifie la fenêtre de commandes : un nouvel écran apparaît avec le nom du projet ouvert dans la zone 5 et 5 boutons dans la zone 1 :

- [qu] pour sortir le projet (retour à la fenêtre de commandes précédente)

- [hp] l’aide

- [am] (resp. [ar] [ai]) pour créer une nouvelle machine abstraite (resp. raffinement ou implémentation)

3.3 Création d’une machine

Pour créer une machine abstraite (ou un MODEL), on clique sur [am] et on entre son nom.

Créez une machine abstraite reservation.

Pour chaque machine créée une nouvelle ligne est ajoutée avec 10 nouveaux boutons et le nom de la machine dont :

- [ed] pour éditer le code source de la machine (dans la zone 2)

- [ty] pour lancer le contrôle syntaxique et de typage de la machine

- [po] pour demander la génération des obligations de preuves

- [rc] pour supprimer la machine

- [p0] (resp. [p1]) pour lancer le prouveur automatique en force 0 (resp. 1)

- [ip] pour lancer le prouveur interactif

La couleur rouge des boutons [ty] et [po] indique que la machine n’est pas correcte (syntaxe et typage) ou que cette vérification n’a pas encore été faite, et que les preuves n’ont pas encore été générées (ou pas régénérées depuis la dernière modification).

Cliquez sur [ed] pour éditer votre machine réservation.

3.4 Edition d’une machine

Rentrez dans la zone 2, la machine suivante :

MODEL

reservation /* service de reservation de places */

VARIABLE

nbPlaceLibre

INVARIANT

nbPlaceLibre : N /* nbPlaceLibre est un entier naturel */

INITIALISATION

nbPlaceLibre := 10

OPERATIONS

reserver =

PRE

nbPlaceLibre > 0

THEN

nbPlaceLibre := nbPlaceLibre - 1

END ;

END

Observez la colorisation des mots clés du langage (qui permet par exemple de voir qu’il faut un S à variable). Observez également que la notation ASCII des symboles est automatiquement transformée en symbole mathématique : seat : N devient seat ( N.

Le menu « B world » d’xemacs au-dessus de la zone 2 permet de retrouver les caractères ASCII associés aux symboles mathématiques et d’insérer facilement tous les éléments du langage B.

Les majuscules sont distinguées des minuscules dans les identificateurs. Un même identificateur ne peut pas être utilisé pour deux objets différents (variable, nom d’opération, machine…). Il est de plus prudent de ne pas utiliser de caractères accentués. Enfin, le nom d’une machine doit correspondre au nom de son composant.

Après chaque modification et avant de déclencher une commande, il est nécessaire de sauver sa machine (bouton save de xemacs au dessus de la zone 2). En particulier, un clic sur [ty] sans sauvegarder auparavant vérifiera la version précédente de la machine et non celle que vous venez de modifier.

Sauver votre machine

3.5 Vérification de syntaxe et de type

Un clic sur [ty] déclenche la vérification de votre machine. Un rapport s’affiche dans la zone 2 (à la place de votre machine). Une succession de pointillés indique que tout est correct !

Déclenchez la vérification

Un message d’erreur vous indique que le dernier point virgule avant le END final est de trop.

Supprimez ce point virgule (cliquez sur [ed] et n’oubliez pas de sauver !) et revérifiez (cliquez sur [ty]).

Un nouveau message vous indique que N est inconnu ! Normal l’ensemble des entiers naturels est désigné par NATURAL (mettez un espace après pour voir apparaître…).

Modifiez, sauvegardez, et revérifiez.

Normalement tout est à présent correct. Le bouton [ty] reste noir.

3.6 Génération des obligations de preuve

Un clic sur [po] déclenche la génération des preuves à démontrer. Un rapport s’affiche en zone 2 indiquant combien de preuves à démontrer ont été générées et combien de preuves triviales (dont la conclusion est dans les hypothèses) ont été produites. De même, le nom du composant en zone 1 est complété