Utilisation de la méthode B et des méthodes formelles en général, pour modéliser et vérifier une liste liée inverse

Question

J'essaie de faire une modélisation formelle d'une liste liée, mais au lieu de référencer le bloc suivant, chaque bloc doit référencer le bloc précédent à la place.

Y a-t-il déjà des méthodes formelles ou des formelles pour ce faire?

Exactement la même chose qu'une liste liée normale, mais lorsqu'un nouveau bloc (valeur etc.) est ajouté, cela fait référence à la valeur passée (un peu comme la blockchain Bitcoin).

J'ai modélisé une liste liée normale (file d'attente de données) modélisée dans la méthode B

MACHINE DataQueue ( DATA , anydata , maxqueue )

CONSTRAINTS anydata E DATA /\ maxqueue > 0
SEES Bool TYPE
SETS TOKEN
PROPERTIES card ( TOKEN ) = maxqueue
VARIABLES TokenSeq , TokenMap

INVARIANT
TokenSeq E iseq ( TOKEN ) /\
TokenMap E TOKEN -|-> DATA /\
dom ( TokenMap )=  USED
INITIALISATION
TokenSeq , TokenMap : [] , {}


OPERATIONS
success , token <-- AddItem( item )  =^
PRE E item DATA THEN
CHOICE
ANY new token WHERE new_token  E TOKEN_USED
THEN
TokenSeq := TokenSeq <-- new token ||
TokenMap ( new token ) := item ||
success , token := TRUE , new token
END
OR
success := FALSE || token :E TOKEN
END
END ;
DEFINITIONS
USED =^ ran ( TokenSeq )
END