Raffinement de la gestion des étudiants avec vérification d'invariants

remove ( st ) =

IF st >=0 ' st<= 100 THEN VAR bb IN bb:= sttab(st);

IF bb= TRUE THEN

sttab ( st ) := FALSE; Nb:=Nb-1

END

END

ENDEND

3/

MACHINE

StudentV2

SETS

STUDENT; NUMBER

/j'ai supprim la constante, d j trait e dans la question pr c dente/

VARIABLES

studentset

INVARIANT

studentset STUDENT NUMBER

INITIALISATION

studentset:={}

OPERATIONS

enter(et)= PRE et STUDENT ' et dom (studentset) ' NUMBER - ran(studentset)`

THEN

ANY nn WHERE nn NUMBER ' nn (ran(studentset)) THEN studentset:=studentset

*{et nn}

END END;

remove(et)=PRE et STUDENT ' et dom(studentset) THEN studentset:=studentset-

{et studentset(et)} END

END

REFINEMENT

StudentV2_r

REFINES

StudentV2

VARIABLES

studentset, numberset

INVARIANT

numberset NUMBER ' numberset=ran(studentset)

INITIALISATION

studentset:=||numberset:=

OPERATIONS

2/7

enter(et)= PRE et STUDENT ' et dom (studentset) ' NUMBER - numberset` THEN

ANY nn WHERE nn NUMBER ' nn numberset THEN studentset:=studentset *{et nn}||

numberset:=numberset* {nn}

END END;

remove(et)=PRE et STUDENT ' et dom(studentset) THEN studentset:=studentset-

{et studentset(et)} || numberset:=numberset- {studentset(et)}END

END

REFINEMENT

StudentV2_2r

REFINES

StudentV2_r

CONCRETE_VARIABLES

studenttab,numbertab

INVARIANT

studenttab STUDENT*NUMBER BOOL ' numbertab NUMBER BOOL '

studentset=dom( studenttab {TRUE}) ' numberset= numbertab{ [{TRUE}]

INITIALISATION

studenttab:=STUDENTNUMBER{FALSE};

numbertab := NUMBER*{FALSE}

OPERATIONS

enter(et)= PRE et STUDENT ' ( nn.(nn NUMBER ' studenttab(et,nn)=TRUE)) '

numbertab {FALSE}` THEN

ANY nn WHERE nn NUMBER ' numbertab(nn)=FALSE THEN

studenttab(et,nn):= TRUE; numbertab(nn):=FALSE

END

END;

remove(et)=PRE et STUDENT ' nn.(nn NUMBER ' studenttab(et,nn)=TRUE) THEN

ANY nn WHERE nn NUMBER ' studenttab(et,nn)= TRUE THEN studenttab(et,nn):= FALSE;

numbertab(nn):= TRUE

END

END

END

IMPLEMENTATION

StudentV2__i

REFINES

StudentV2_2r

VALUES

STUDENT = 0..100; NUMBER=0..150

INITIALISATION

studenttab:=STUDENTNUMBER{FALSE};

numbertab := NUMBER*{FALSE}

OPERATIONS

enter(et)=

IF et>=0 ' et<=100 THEN

VAR cpt, bb IN

/v rifier qu'on a pas d j affecter un num ro cet tudiant et/

cpt:=0; bb:=studenttab(et,cpt);

WHILE bb=FALSE ' cpt<150 DO

cpt:=cpt+1; bb:=studenttab(et,cpt)

INVARIANT

cpt NUMBER ' bb BOOL ' nb. (nb NAT ' nb>= 1 ' nb <= cpt-1

studenttab(et, nb)=FALSE)

VARIANT

150-cpt

END;

/*si l' tudiant n'a pas de num ro il faudra chercher le premier num ro libre pour le lui

affecter*/

IF bb=FALSE THEN

cpt:=0; bb:=numbertab(cpt);

WHILE bb=TRUE ' cpt<150 DO

3/7

cpt:=cpt+1; bb:=numbertab(cpt)

INVARIANT

cpt NUMBER ' bb BOOL ' numbertab[1..cpt-1] {TRUE}

VARIANT

150-cpt

END;

IF bb=FALSE THEN studenttab(et,cpt):= TRUE; numbertab(cpt):=TRUE

END

END

END

END;

remove(et)=

IF et>=0 ' et<=100 THEN

/v rifier qu'on a d j affect un num ro cet tudiant et/

VAR cpt, bb IN

cpt:=0; bb:=studenttab(et,cpt);

WHILE bb=FALSE ' cpt<150 DO

cpt:=cpt+1; bb:=studenttab(et,cpt)

INVARIANT

cpt NUMBER ' bb BOOL ' nb. (nb NAT ' nb>= 1 ' nb <= cpt-1

studenttab(et, nb)=FALSE)

VARIANT

150-cpt

END;

/si on a d j affect un num ro cet tudiant alors l'annuler/

IF bb=TRUE THEN studenttab(et,cpt):= FALSE; numbertab(cpt):=TRUE

END

END

END END

Exercice 3 : M moire

1. Sp cifier une machine dallocation dun mot dans une m moire. Cette

machine comporte lop ration allouer qui retourne ladresse de lemplacement

allou , sil y a de la place en m moire.

2. Raffiner la machine abstraite obtenue jusqu aboutir une impl mentation.

3. Ecrire et calculer les obligations de preuve.

MACHINE

Memoire

SETS

ADRESSES

CONSTANTS

null,mem

PROPERTIES

mem ADRESSES ' null ADRESSES ' null mem

VARIABLES

alloues

INVARIANT

alloues mem

INITIALISATION

alloues := {}

OPERATIONS

adr <-- allouer=

IF mem - alloues ` {} THEN

ANY aa WHERE aa mem - alloues THEN adr:= aa || alloues:=alloues * {aa} END

ELSE

adr:=null

END

END

REFINEMENT

Memoire_r

4/7

REFINES

Memoire

CONCRETE_VARIABLES

tabAllocation

INVARIANT

tabAllocation mem BOOL ' alloues=tabAllocation{ [{TRUE}]

INITIALISATION

tabAllocation := mem*{FALSE}

OPERATIONS

adr <-- allouer =

IF tabAllocation {FALSE}`

THEN

ANY aa

WHERE

aa mem ' tabAllocation(aa)=FALSE

THEN

adr := aa || tabAllocation(aa):=FALSE

END

ELSE

adr := null

END

END

IMPLEMENTATION

Memoire_i

REFINES

Memoire_r

VALUES

ADRESSES = 0..20000 ;

null = 0 ;

mem = 1 .. 2000

INITIALISATION

VAR ind IN

ind := 1;

WHILE ind <= 2000 DO

tabAllocation(ind):=FALSE;ind := ind + 1

INVARIANT

ind mem ' tabAllocation[1..ind - 1] {FALSE}

VARIANT 2001 - ind

END

END / c'est quivalent tabAllocation := mem{FALSE}*/

OPERATIONS

adr <-- allouer =

VAR ind, val IN

ind := 1; val := tabAllocation(ind);

WHILE ind < 2000 ' val = TRUE DO

ind := ind + 1;

val := tabAllocation(ind)

INVARIANT

ind mem ' val BOOL ' tabAllocation[1..ind - 1] {TRUE}

VARIANT 2000 - ind

END;

IF val=FALSE THEN adr := ind ; tabAllocation(ind) := TRUE

ELSE adr :=null

END

END END

Exercice4

Premi re solution : d clarer la fontion Suiv comme tant une constante abstraite

MACHINE

Carrefour

SETS

COULEUR = {rouge, jaune, vert}

ABSTRACT_CONSTANTS

Suiv

PROPERTIES

Suiv COULEUR COULEUR '

5/7

Suiv(rouge) = vert '

Suiv(vert) = jaune '

Suiv(jaune) = rouge

VARIABLES

feuA, feuB

DEFINITIONS

hs == feuA = jaune ' feuB = jaune;

service(aa,bb) == (aa = rouge ' bb ` rouge) or (aa ` rouge ' bb = rouge);

es == service(feuA, feuB)

INVARIANT

feuA, feuB COULEUR * COULEUR ' (hs or es)

INITIALISATION

feuA, feuB := jaune, jaune

OPERATIONS

Mise_en_service = PRE hs

THEN ANY fa, fb WHERE

fa COULEUR ' fb COULEUR ' (service(fa,fb))

THEN

feuA := fa||feuB := fb

END

END;

Mise_hors_service = PRE es

THEN

feuA, feuB := jaune, jaune

END;

Changer_feu = PRE es

THEN

ANY fa, fb WHERE fa COULEUR ' fb COULEUR '

((fa = feuA ' fb = Suiv(feuB)) or

(fa = Suiv(feuA) ' fb = feuB) or

(fa = Suiv(feuA) ' fb = Suiv(feuB)) '

(service(fa,fb)))

THEN

feuA, feuB := fa, fb

END

END

END

REFINEMENT

Carrefour_r

REFINES

Carrefour

CONCRETE_VARIABLES

feuA ,

feuB

DEFINITIONS

hs == feuA = jaune & feuB = jaune ;

es == service ( feuA , feuB );

service ( aa , bb ) == ( aa = rouge & bb /= rouge ) or ( aa /= rouge & bb = rouge )

INITIALISATION

feuA , feuB := jaune , jaune

OPERATIONS

Mise_en_service =

PRE

hs

THEN

feuA := rouge || feuB := vert

END;

Changer_feu =

PRE

es

THEN

SELECT feuA = vert ' feuB= rouge THEN feuA := jaune

WHEN feuA = jaune & feuB = rouge THEN feuA:=rouge; feuB:=vert

WHEN feuA = rouge & feuB = vert THEN feuB := jaune

WHEN feuA = rouge & feuB = jaune THEN feuA:= vert; feuB := rouge

6/7

END

END

END

IMPLEMENTATION

&

Remarque : SELECT est une substitution non d terministe, il faudra lever le non-

d terminisme et la remplacer par une substitution d terministe (IF).

Rappel : dans limpl mentation on ne peut utiliser que les substitutions d terministes :

IF, CASE, WHILE, ; , VAR

7/7