Question

I have created a very basic model of an array list in the B method as shown below

MACHINE Array(TYPE)

VARIABLES block

INVARIANT block : seq(TYPE)

INITIALISATION block := []

OPERATIONS

add(e) =
   PRE e : TYPE
   THEN block := block <- e
   END;

remove =
   PRE block /= []
   THEN block := tail(block)
   END;

res <-- showArray =
    res := block;

res <-- getfront =
   PRE block /= []
   THEN res := first(block)
   END

END

However what I am trying to achieve is to create a model that prevents deletion from the list, so when an element is added, it cannot be deleted.

What should I add in the invariant to achieve this?

No correct solution

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