Come prevenire la cancellazione in un array nel metodo B

Question

Ho creato un modello molto semplice di un elenco di array nel metodo B come mostrato di seguito

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

Tuttavia, ciò che sto cercando di ottenere è creare un modello che impedisca la cancellazione dall'elenco, quindi quando viene aggiunto un elemento, non può essere eliminato.

Cosa devo aggiungere l'invariante per raggiungere questo obiettivo?