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

Exercice 1 - Maximum

Conformément au document source de l'examen, la correction de cet exercice a été entièrement traitée dans le cours. Aucune solution spécifique n'est fournie dans l'énoncé pour cette partie.

Exercice 2 - Students

Le document source numérote les parties de cet exercice « 1/ » et « 3/ ». La partie 2/ est absente du texte original ; nous passerons donc directement de la première spécification à la version 2 traitée dans la troisième partie.

Note sur la syntaxe : Le code extrait du document utilise des symboles mathématiques théoriques (∈, ∧, ∪, ↦, ▷). Afin de garantir que le code fourni soit exécutable et valide dans un prouveur comme Atelier B, ces symboles ont été transcrits dans la syntaxe ASCII standard du langage B (par exemple : pour l'appartenance, & pour le ET logique, \/ pour l'union, |-> pour les couples, et |> pour la restriction au co-domaine). De même, les accès aux tableaux à deux dimensions du type studenttab(et, nn) ont été corrigés en studenttab(et |-> nn).

Exercice 2 - Partie 1 : Modélisation et implémentation simples

La première approche modélise un ensemble d'étudiants (studentset) dont la taille est limitée par une constante maxi.

Machine abstraite : La machine s'assure que le nombre d'étudiants ne dépasse jamais maxi. L'opération enter vérifie que l'étudiant n'est pas déjà présent et qu'il reste de la place.

MACHINE
    Student
SETS
    STUDENT
CONSTANTS
    maxi
PROPERTIES
    maxi : NAT
VARIABLES
    studentset
INVARIANT
    studentset <: STUDENT & card(studentset) <= maxi
INITIALISATION
    studentset := {}
OPERATIONS
    enter(st) = 
    PRE 
        st : STUDENT & st /: studentset & card(studentset) < maxi 
    THEN
        studentset := studentset \/ {st} 
    END;
    
    remove(st) = 
    PRE 
        st : STUDENT & st : studentset 
    THEN 
        studentset := studentset - {st} 
    END
END

Raffinement : On raffine l'ensemble abstrait par un tableau concret de booléens (sttab). L'invariant de collage explicite que studentset correspond à l'image inverse de {TRUE} par la fonction sttab (noté sttab~[{TRUE}] en syntaxe B).

REFINEMENT
    Student_r
REFINES
    Student
VARIABLES
    sttab
INVARIANT
    sttab : STUDENT --> BOOL & studentset = sttab~[{TRUE}]
INITIALISATION
    sttab := STUDENT * {FALSE}
OPERATIONS
    enter(st) =
    PRE
        st : STUDENT & sttab(st) /= TRUE & card(sttab~[{TRUE}]) < maxi
    THEN
        sttab(st) := TRUE
    END;
    
    remove(st) =
    PRE
        st : STUDENT & sttab(st) = TRUE
    THEN
        sttab(st) := FALSE
    END
END

Implémentation : L'implémentation introduit des valeurs concrètes (0 à 100 pour STUDENT) et ajoute une variable redondante Nb pour garder une trace du nombre d'étudiants inscrits sans avoir à calculer la cardinalité à chaque fois. Les préconditions (PRE) deviennent des conditions opérationnelles (IF).

IMPLEMENTATION
    Student_i
REFINES
    Student_r
VALUES
    STUDENT = 0..100; maxi = 20
CONCRETE_VARIABLES
    Nb, sttab
INVARIANT
    Nb : 0..maxi & card(sttab |> {TRUE}) = Nb
INITIALISATION
    sttab := STUDENT * {FALSE}; 
    Nb := 0
OPERATIONS
    enter(st) =
    IF st >= 0 & st <= 100 THEN 
        VAR bb IN 
            bb := sttab(st);
            IF bb = FALSE & Nb < maxi THEN
                sttab(st) := TRUE; 
                Nb := Nb + 1
            END 
        END
    END;
    
    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
    END
END

Exercice 2 - Partie 3 : Numérotation des étudiants

Cette version (StudentV2) modélise l'association d'un numéro unique à chaque étudiant. L'ensemble devient une fonction partielle injective (>+>). L'énoncé indique la suppression de la constante maxi, cette dernière ayant été traitée précédemment.

Machine abstraite (V2) :

MACHINE
    StudentV2
SETS
    STUDENT; NUMBER
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

Premier raffinement (V2_r) : On sépare le domaine et l'image de la fonction en deux entités pour préparer l'implémentation de la recherche de numéros libres.

REFINEMENT
    StudentV2_r
REFINES
    StudentV2
VARIABLES
    studentset, numberset
INVARIANT
    numberset <: NUMBER & numberset = ran(studentset)
INITIALISATION
    studentset := {} || numberset := {}
OPERATIONS
    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

Second raffinement (V2_2r) : On transforme les ensembles en tableaux de booléens (studenttab pour la relation étudiant-numéro et numbertab pour la disponibilité des numéros).

REFINEMENT
    StudentV2_2r
REFINES
    StudentV2_r
VARIABLES
    studenttab, numbertab
INVARIANT
    studenttab : STUDENT * NUMBER --> BOOL & 
    numbertab : NUMBER --> BOOL &
    studentset = dom(studenttab |> {TRUE}) & 
    numberset = numbertab~[{TRUE}]
INITIALISATION
    studenttab := STUDENT * NUMBER * {FALSE};
    numbertab := NUMBER * {FALSE}
OPERATIONS
    enter(et) = 
    PRE 
        et : STUDENT & not(#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) := TRUE
        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) := FALSE
        END
    END
END

Note sur la source : Dans l'opération remove, l'énoncé source écrivait numbertab(nn):= TRUE après libération du numéro. La logique correcte (libérer le numéro) et la cohérence avec le reste des invariants dictent qu'un numéro non assigné soit à FALSE, j'ai donc reporté FALSE ici pour que l'état soit valide.

Implémentation finale (V2__i) : Traduction en algorithmique stricte en utilisant des boucles WHILE pour simuler le quantificateur existentiel et chercher les numéros libres.

IMPLEMENTATION
    StudentV2__i
REFINES
    StudentV2_2r
VALUES
    STUDENT = 0..100; 
    NUMBER = 0..150
INITIALISATION
    studenttab := STUDENT * NUMBER * {FALSE};
    numbertab := NUMBER * {FALSE}
OPERATIONS
    enter(et) =
    IF et >= 0 & et <= 100 THEN
        VAR cpt, bb IN
            /* vérifier qu'on n'a pas déjà affecté un numéro à cet étudiant */
            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;
            
            /* s'il n'a pas de numéro, chercher le premier libre */
            IF bb = FALSE THEN
                cpt := 0; 
                bb := numbertab(cpt);
                WHILE bb = TRUE & cpt < 150 DO
                    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
        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;
            
            IF bb = TRUE THEN 
                studenttab(et |-> cpt) := FALSE; 
                numbertab(cpt) := FALSE
            END
        END
    END
END

Exercice 3 - Mémoire

Exercice 3 - Question 1 : Spécification abstraite

La spécification requiert une opération allouer qui retourne une adresse mémoire si possible, ou null sinon.

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

Exercice 3 - Question 2 : Raffinements et implémentation

On utilise un tableau d'allocation booléen pour représenter l'occupation mémoire.

Raffinement :

REFINEMENT
    Memoire_r
REFINES
    Memoire
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) := TRUE
        END
    ELSE
        adr := null
    END
END

Note sur la correction : L'énoncé source écrivait tabAllocation(aa):=FALSE lors de l'allocation d'une adresse libre. Il s'agit d'une erreur typographique courante. Le but d'une allocation étant de marquer l'espace comme occupé, l'instruction a été corrigée en tabAllocation(aa) := TRUE pour correspondre à la logique de l'invariant (alloues = tabAllocation~[{TRUE}]).

Implémentation :

IMPLEMENTATION
    Memoire_i
REFINES
    Memoire_r
VALUES
    ADRESSES = 0..20000;
    null = 0;
    mem = 1..2000
CONCRETE_VARIABLES
    tabAllocation
INITIALISATION
    VAR ind IN
        ind := 1;
        WHILE ind <= 2000 DO
            tabAllocation(ind) := FALSE;
            ind := ind + 1
        INVARIANT
            ind : mem \/ {2001} & tabAllocation[1..ind - 1] <: {FALSE}
        VARIANT 
            2001 - ind
        END
    END
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

Exercice 3 - Question 3 : Obligations de preuve

L'énoncé demande de « Ecrire et calculer les obligations de preuve ». Bien que la question soit posée, le corrigé source ne contient ni la liste formelle des obligations de preuve (calcul de [S]I), ni leur démonstration mathématique. Conformément à la règle de ne pas inventer d'information absente du document, il faut noter que ces calculs sont manquants dans la copie fournie.

Exercice 4 - Carrefour

Cet exercice modélise la logique de contrôle d'un feu de carrefour à trois couleurs, gérant deux voies (feuA et feuB).

Première solution - Machine abstraite :

MACHINE
    Carrefour
SETS
    COULEUR = {rouge, jaune, vert}
ABSTRACT_CONSTANTS
    Suiv
PROPERTIES
    Suiv : COULEUR --> COULEUR &
    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 : COULEUR & feuB : COULEUR & (hs or es)
INITIALISATION
    feuA := jaune || feuB := 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 := jaune || feuB := 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 := fa || feuB := fb
        END
    END
END

Raffinement :

Le raffinement lève le non-déterminisme abstrait (le constructeur ANY) en explicitant les transitions d'état de Mise_en_service et Changer_feu.

REFINEMENT
    Carrefour_r
REFINES
    Carrefour
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 := jaune || feuB := 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
        END
    END
END

Implémentation :

Le document source laisse le bloc d'implémentation vide (IMPLEMENTATION …) et s'accompagne d'une consigne formelle justifiant ce vide. L'implémentation complète n'est donc pas fournie, mais la méthode pour l'obtenir est dictée par la remarque suivante tirée du document original :

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 l'implémentation on ne peut utiliser que les substitutions déterministes : IF, CASE, WHILE, ;, VAR.

Méthode

Pour aborder ce type d'épreuve sur la méthode B :

1. Syntaxe et sémantique : Gardez toujours à l'esprit la différence entre la syntaxe de la machine abstraite (qui autorise le non-déterminisme avec ANY, les préconditions avec PRE, les actions simultanées avec ||) et celle de l'implémentation (qui exige un algorithme pas-à-pas avec des IF, des boucles WHILE, et des instructions séquentielles ;).
2. Gestion des erreurs matérielles : Les erreurs courantes dans les copies (comme affecter FALSE alors qu'on réserve un espace dans l'Exercice 3) rendent vos théorèmes improuvables. Vérifiez méticuleusement que les actions de vos opérations maintiennent la vérité définie dans l'INVARIANT.
3. Traduction des propriétés mathématiques : Un quantificateur existentiel (∃) dans un invariant ou une précondition devient inévitablement une boucle de recherche (WHILE) dans l'implémentation. Soyez prêt à formuler l'invariant de cette boucle : il affirme généralement qu'avant l'indice actuel, l'élément cherché n'a pas été trouvé (ex: tab[1..ind-1] <: {FALSE}).
4. Cohérence du raffinement : Lorsqu'une machine relie un ensemble à des booléens ou à des numéros, assurez-vous d'utiliser une variable de collage (studentset = sttab~[{TRUE}]). Elle est essentielle au prouveur pour démontrer que la logique concrète respecte les limites fixées dans l'abstraction.