Comment empêcher la suppression dans un tableau dans la méthode B

Question

J'ai créé un modèle très basique d'une liste de tableaux dans la méthode B comme indiqué ci-dessous

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

Cependant, ce que j'essaie de réaliser, c'est de créer un modèle qui empêche la suppression de la liste, donc lorsqu'un élément est ajouté, il ne peut pas être supprimé.

Que dois-je ajouter l'invariant pour y parvenir?