1
$\begingroup$

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
$\endgroup$
3
$\begingroup$

There are many approaches for verifying linked structures---arguably, more suitable than the B method---that you might want to use, depending on the language and properties you want to verify. Most of the approaches rely on separation logic (which was in big part motivated for verification of linked structures).

Some tools include:

To quote this answer (which answers a very similar question), even though you did not give details about what are you trying to verify, it seems that properties you might want to prove about the "reverse linked list" might be formulated as properties for a regular linked list. (If the reverse list requires some additional (non-standard) implementations, not already declared for the linked list, you might be able to model those in addition.)

I am not sure what was the purpose of your example, but your code seems similar to an example of modelling a linked list with B (which includes other standard operations) method in Program Development by Refinement Case Studies Using the B Method.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.