Question

I am trying to do some formal modeling of a linked list, however instead of referencing the next block, each block needs to reference the previous block instead.

Is there already any formal methods or any formal for doing this ?

Exactly the same as a normal linked list but when a new block (value etc) is added this references the past value (much like the bitcoin blockchain).

I have modeled a normal linked list (Data queue) modeled in the b method

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

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top