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

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

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

res &lt;-- showArray =
    res := block;

res &lt;-- 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?
You cannot add such a property to your invariant because the invariant describes how a valid state might look like but not how it can be altered.

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.

Every valid refinement is then not allowed to remove an element.