# How to prevent deletion in an array in the B method

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

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?

The operations are responsible for specifying the behaviour of the model. If you want to prevent that an element will be removed from the array, just do not specify that as a possible behaviour. In your example above, just remove the operation remove.
Add a postcondition to each operation stating that if the array held an element before the operation, then the element is still present afterwards. In other words, if $A[i]=x$ held before the operation, then $A[i]=x$ still holds. I'll let you work out how to express this in formal mathematics and prove by induction that this achieves what you want, since this is your exercise.