Utilizzo di B-Method e metodi formali in generale, per modellare e verificare un elenco collegato inverso

Question

Sto cercando di fare una modellazione formale di un elenco collegato, tuttavia invece di fare riferimento al blocco successivo, ogni blocco deve invece fare riferimento al blocco precedente.

Esistono già metodi formali o formali per farlo?

Esattamente lo stesso di un normale elenco collegato ma quando viene aggiunto un nuovo blocco (valore ecc.) Questo riferisce il valore passato (proprio come la blockchain Bitcoin).

Ho modellato un normale elenco collegato (coda di dati) modellato nel metodo 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