Exemple : un carnet d'anniversaire

B Exemple : un carnet d'anniversaire

B.1 Modélisation

Nous allons étudier comment modéliser un carnet d'anniversaires.

Le carnet doit contenir pour un ensemble de personnes, leur nom et la date de leur anniversaire. Les opérations possibles sur le carnet sont :

ajouter un nom et une date anniversaire
trouver la date anniversaire d'une personne
trouver toutes les personnes dont l'anniversaire est un certain jour.

On suppose de plus que le nombre maximal de personnes pouvant être entrées dans le carnet est fixé.

On choisit de modéliser le carnet par une machine paramétrée par deux ensembles NOM et DATE représentant respectivement les univers des noms des personnes et des dates, ainsi qu'un entier max qui représente le nombre maximal d'entrées dans le carnet.

Une modélisation possible est la suivante :

MACHINE CarnetAnniversaires(NOM,DATE,maxn)

CONSTRAINTS maxn : N₁

VARIABLES connus,anniversaire

INVARIANT

connusÍ NOM Ù card(connus) £ maxn Ù anniversaireÎ connus >-> DATE

INITIALISATION connus,anniversaire:=Ø,Ø

OPERATIONS

ajout(n,a) =

PRE nÎNOM-connus Ù a Î DATE Ù card(connus)<maxn

THEN connus:=connusÈ{n} ||anniversaire(n):=a END

a¬¾trouve(n) =

PRE nÎ connus THEN a:=anniversaire(n) END

ns ¬¾a_feter(j) =

PRE jÎ DATE THEN ns:=anniversaire^-1[{j}] END

END

On peut vérifier que les différentes préconditions des opérations permettent d'assurer que l'invariant de la machine est bien préservé.

B.2 Machine défensive

Cependant les opérations de cette machine ont des conditions d'utilisation trop restrictives: ce n'est pas à l'utilisateur de s'assurer que le nom qu'il ajoute n'est pas dans la base, que la base n'est pas pleine ou que le nom qu'il cherche est bien dans la base.

Pour remédier à ce problème, on modifie les opérations de manière à ce que chaque opération renvoie un indicateur si l'opération a pu se dérouler normalement et un autre indicateur si une erreur s'est produite. On utilisera un indicateur différent pour chaque type d'erreur. On peut faire une analogie avec les codes de retour des fonctions unix, ou un mécanisme paramétré d'erreurs.

On choisit d'introduire une nouvelle machine CarnetAnniversairesI qui aura les mêmes variables que la machine CarnetAnniversaires mais qui contiendra un nouvel ensemble RAPPORT ainsi que de nouvelles opérations pour l'ajout ou la consultation renvoyant les rapports apropriés. Comme cette nouvelle machine a les mêmes variables d'état que l'ancienne machine, il est possible d'utiliser une déclaration INCLUDES.

MACHINE CarnetAnniversairesI(NOM,DATE,max)

CONSTRAINTS maxn : N₁

INCLUDES CarnetAnniversaires(NOM,DATE,max)

SETS RAPPORT={ok,deja_connu,inconnu,plein}

OPERATIONS

r¬¾ ajoutI(n,a) =

PRE nÎNOM Ù a Î DATE THEN

IF nÏconnus THEN

IF card(connus)<maxn THEN ajout(n,a)||r:=ok ELSE r:=plein END

ELSE r:=deja_connu END

END;

r,a¬¾trouveI(n) =

PRE nÎ NOM THEN

IF nÎ connus THEN (r,a):=(ok,trouve(n))

ELSE r :=inconnu || a:Î DATE END

END;

r,ns ¬¾a_feterI(j) = PRE jÎ DATE THEN ns¬¾ a_feter(j) || r:= ok END

END

B.3 Raffinement

Le raffinement transforme les ensembles de noms et la relation d'anniversaire en deux tableaux partageant les mêmes indices.

REFINEMENT CarnetAnniversairesRI

REFINES CarnetAnniversairesI

VARIABLES noms, dates, index

INVARIANT

indexÎ 0..maxn Ù nomsÎ 1..index >-> NOM Ù datesÎ 1..index >-> DATE

Ù connus=ran(noms)

Ù " x,y. (x |® y) Î anniversaire Û $ i. i Î 1..index Ù noms(i)=x Ù dates(i)=y

INITIALISATION index,noms,dates:=0,Ø,Ø

OPERATIONS

r¬¾ ajoutI(n,a) =

PRE nÎNOM Ù a Î DATE THEN

IF nÏran(noms) THEN

IF index<maxn

THEN noms(index+1):=n || dates(index+1):=a ||

index:= index+1 ||r:=ok

ELSE r:=plein END

ELSE r:=deja_connu END

END;

r,a¬¾trouveI(n) =

PRE nÎ NOM

THEN

IF nÎ ran(noms) THEN (r,a):=(ok,dates(noms^-1(n)))

ELSE r:=inconnu || a:Î DATE END

END;

r,ns ¬¾a_feterI(j) =

PRE jÎ DATE THEN ns¬¾ ns:=noms[dates^-1[{j}]]|| r:= ok END

END

B.4 Implantation

Pour traiter notre exemple, nous pouvons en particulier utiliser une machine Arr qui encapsule un tableau (variable arr avec des opérations d'accès et de mise à jour) et une machine Nvar pour implanter une variable entière var. On utilise deux tableaux (l'un pour les noms, l'autre pour les dates), lors de l'import, un préfixe permet de distinguer les deux instances.

B.4.1 Machine auxilliaire : variable

Pour la machine qui implante une variable entière, nous utilisons des opérations de lecture et d'incrémentation.

La spécification de la machine Nvar est la suivante :

MACHINE Nvar(maxn)

CONSTRAINTS maxn : N₁

VARIABLES nvar

INVARIANT nvarÎ 0..maxn

INITIALISATION nvar:=0

OPERATIONS

v¬¾ val_nvar = v:=nvar;

inc_nvar =

PRE nvar < maxn THEN nvar:=nvar+1 END;

END

B.4.2 Tableaux

Pour les tableaux, nous aurons besoin des opérations d'accès à une valeur, de mise à jour ainsi que d'une fonction de recherche d'un élément dans un sous-ensemble du tableau. Cette opération renvoie un booléen qui dit si l'élément a été trouvé et dans le cas positif renvoie le plus petit indice où l'élément figure.

MACHINE Arr(TYPE,maxn)

CONSTRAINTS maxn : N₁

SEES Bool_TYPE

VARIABLES arr

INVARIANT arrÎ 1..maxn +-> TYPE

INITIALISATION arr:=Ø

OPERATIONS

v¬¾ val_arr(i) = PRE i Î dom(arr) THEN v:=arr(i) END;

sto_arr(i,v) =

PRE i Î 1..maxn Ù v Î TYPE THEN arr(i):=v END;

b,k¬¾ ch_eql_arr(i,j,v) =

PRE i..j Í dom(arr) Ù i £ j Ù v Î TYPE THEN

IF vÎ arr[i..j]

THEN b:=TRUE ||

k: (k Î i..j Ù arr(k)=v Ù " l. lÎ i..(k-1) Þarr(l)¹v)

ELSE b:=FALSE||k:ÎTYPE

END

END

B.4.3 Implantation du carnet

Nous pouvons alors écrire l'implémentation de la machine des carnets d'adresse.

IMPLEMENTATION CarnetAnniversairesRII

REFINES CarnetAnniversairesRI

IMPORTS noms_Arr(NOM,max), dates_Arr(DATE,max), index_Nvar(max)

SEES Bool_TYPE

INVARIANT

index = index_nvar

Ù noms = 1..index <| noms_arr

Ù dates = 1..index <| dates_arr

OPERATIONS

r¬¾ ajoutI(n,a) = VAR b,i,j IN

j¬¾ index_val_nvar;

IF j¹0 THEN b,i¬¾noms_ch_eql_arr(1,j,n) END;

IF j=0Ú b=FALSE THEN

b¬¾index_neq_nvar(maxn);

IF b=TRUE

THEN noms_sto_arr(j+1,n); dates_sto_arr(j+1,a);

index_inc_nvar; r:=ok

ELSE r:=plein END

ELSE r:=deja_connu END

END;

r,a¬¾trouveI(n) =

VAR b,i,j

IN j¬¾ index_val_nvar;

IF j¹0 THEN b,i¬¾noms_ch_eql_arr(1,j,n)

ELSE b:=FALSE; i:=maxn END;

IF b=TRUE THEN r:=ok

ELSE r:=inconnu END

a¬¾ dates_val_arr(i)

END;

L'opération de recherche des fêtes à souhaiter ne peut pas être implantée directement car c'est une opération qui nécessite de calculer un ensemble de valeurs, ce qui n'est pas possible directement en B. Une solution est de stocker une séquence des noms des personnes dont c'est l'anniversaire puis d'avoir une opération de lecture de cette séquence nom par nom. Nous appelons collect cette nouvelle opération qui sera spécifiée à l'aide d'une variable abstraite fetes et implantée à l'aide d'une séquence fetes_Seq. L'invariant nous assure l'égalité des deux objets.

collect(jo) =

VAR b,i,j,k

IN j¬¾ index_val_nvar; fetes_clr_seq; i:=0

WHILE i¹j DO

i:=i+1;(b,i)¬¾dates_ch_eql_arr(i,j,jo);

IF b=TRUE THEN k:=noms_val_arr(i); fetes_psh_seq(k)

ELSE i:=j

END

VARIANT j-i

INVARIANT i Î N Ù j Î N Ù 0 £ i Ù i £ j Ù j = index

Ù fetes_seq[1..i] = 1..i <| nom[dates^-1[{jo}]] Ù size(fetes_seq)£ i

END

END;