dico

/* Dico
 * Author: brancharel romain
 * Creation date: 15/01/20
 */
MACHINE
    Dico
 SETS
    MOT /*enssemble de mots*/
;   SIGNIFIK = {s0,s1,s2,s3} /*ensemble des significations*/

CONSTANTS
    maxMots /*nombre de mots max du dico */

PROPERTIES
    maxMots : 1..MAXINT

VARIABLES
    listeMots /*liste de mots du dico*/
,   dico /*dictionnaire (mot->signification)*/

INVARIANT
    listeMots : FIN(MOT) /*ensemble fini représentant la liste des mots ajouté*/
&   dico : listeMots --> SIGNIFIK /*le dico fait la relation entre un mot et une signification */
&   card(listeMots) <= maxMots /*le sous enssemble listMots ne doit pas dépaser le nombre de mots max*/

INITIALISATION
    listeMots := {}
||  dico := {}

OPERATIONS
    ajoutMot(mm, signif) =
        PRE
            /*le mot appartient a l'ensemble des mots mais n'appartient pas a la listMots*/
            mm : MOT
            &    mm /: listeMots
            /*la signif appartient a l'ensemble des signification mais la relation mm->signif n'appartient pas au dico*/
            &    signif : SIGNIFIK
            &    (mm,signif) /: dico
            /*le nombre maximal de mot n'est pas dépassé*/
            &    card(listeMots) < maxMots
        THEN
            listeMots := listeMots \/ {mm}
            ||    dico(mm) := signif
        END
    ;

    RetraitMot(mm) =
        PRE
            mm : MOT
            &    mm : dom(dico)
            &    card(listeMots) > 1
        THEN
            listeMots := listeMots - {mm}
            ||    dico := {mm} <<| dico
        END
    ;

    ex <-- existeMot(mm) =
        PRE
            mm : MOT
        THEN
            ex := bool(mm : dom(dico))
        END
    ;

    res <-- rechercheSignifMot(mm) =
        PRE
            mm : MOT
            &    mm : dom(dico)
        THEN
            res := dico(mm)
    END
END