Que signifie la «monotonie» dans le contexte de la mutabilité

Je lis le langage de programmation Rust et j'ai trouvé le passage suivant:

N'oubliez pas que l'écriture dans une structure n'est pas une opération atomique, et de nombreuses fonctions comme vec.push()peuvent se réallouer en interne et provoquer un comportement dangereux, donc même la monotonie peut ne pas être suffisante pour justifier UnsafeCell

Il vient de sortir de nulle part dans le livre et j'ai eu du mal en ligne à essayer de trouver ce que cela signifie exactement dans ce contexte. Trop d'informations concernent le concept de "monotonie" des fonctions mathématiques, que je connaissais déjà mais qui n'est apparemment pas très utile.

Il me semblait seulement trouver cet article qui en parle.

Maintenant, en plus de respecter l'égalité de manière évidente, j'inclus également la stipulation qu'un programme fonctionnel doit respecter la monotonie des observations. Qu'est-ce que je veux dire par là? Ce doit être qu'une fois que vous avez observé quelque chose à un moment donné, alors cela ne cessera pas d'être évident à l'avenir. Ceci est analogue à la propriété de monotonie dans la sémantique de Kripke ou Beth.

Cependant, c'est aussi assez abstrait et je ne suis pas sûr que cela parle de la même chose non plus.

L'auteur semble utiliser le même concept (général) de «monotonie» qu'en mathématiques pures.

En utilisant l'exemple de a vector, si la taille d'une instance particulière de vectorest monotone, il semblerait raisonnable de supposer que l'emplacement de mémoire de tout pushélément précédemment éd ne sera pas modifié par la suite, et donc qu'il est sûr de changer directement la valeur de cet élément sans avoir à se synchroniser avec les opérations vectorultérieures du push.

Cette hypothèse semble raisonnable pour la même raison pour laquelle il semble raisonnable de supposer que l'emplacement de mémoire d'un élément précédemment poussé sur une pile (non circulaire, basée sur un tableau, non bornée) dont la taille augmente strictement ne sera pas affecté par un futur pushopération. Cela contraste avec une pile sur laquelle les opérations pushet les deux popsont appelées, et donc l'emplacement de mémoire d'un élément précédemment poussé peut être "supprimé" par une popopération, et donc disponible pour être affecté à nouveau (c'est-à-dire modifié) par un pushopération ultérieure .

Le point de l'auteur est que cette hypothèse n'est pas correcte, car même dans une structure de données dont la taille est strictement croissante, les insertions futures peuvent affecter les éléments précédemment insérés en déclenchant une réallocation interne d'une sorte qui est distincte de l'effet "logique" de l'insertion .