Pourquoi cet invariant devient-il faux?

Question

En lecture accélérés C++ j'ai été confondu par l'explication donnée pour laquelle l'invariant devient fausse (voir code ci-dessous):

L'invariant est défini par l'auteur (dans ce cas) comme:

Le invariant pour notre temps est que nous avons écrit r lignes de sortie jusqu'à présent. Quand nous définissons r, nous lui donnons une valeur initiale de 0. A ce stade, nous n'avons rien écrit du tout. Mettre r à 0 rend évidemment l'invariant vrai, donc nous avons rencontré la première exigence.

// invariant: we have written r rows so far 
int r = 0; 

// setting r to 0 makes the invariant true 
while (r != rows) { 
    // we can assume that the invariant is true here 

    // writing a row of output makes the invariant false <- WHY? 
    std::cout << std::endl; 

    // incrementing r makes the invariant true again 
    ++r; 
} 
// we can conclude that the invariant is true here 

Alors explique plus tard ...

Rédaction d'une ligne de sortie provoque l'invariant de devenir faux, parce que r n'est plus le nombre de lignes que nous avons écrit

Étant donné la définition, je ne peux pas établir une connexion entre les deux.

Pourquoi l'invariant devient-il faux lorsqu'une ligne de sortie écrit?

Answer 1

r est défini comme étant le nombre de lignes qui ont été imprimées. Par conséquent, l'invariant est vrai que lorsque

r == number of rows that have been printed 

Entre lorsque vous imprimez une ligne et lorsque vous incrémenter r de mettre à jour le nombre de lignes imprimées jusqu'à présent, que invariant est pas vrai.

r est égal à un certain nombre (disons, n), et le « nombre de lignes qui ont été imprimées » est un plus grand que ce nombre (n + 1), en raison de la ligne que vous venez d'imprimer. Par conséquent, l'invariant n'est pas vrai car n != n + 1.

Answer 2

nous avons écrit des lignes de r de la production jusqu'à

r commence à 0 et au point où le cout est r est toujours 0. Le cout a écrit 1 ligne, mais r est 0. Par conséquent, l'invariant est temporairement faux parce que si vous branchez la valeur de r dans la déclaration ci-dessus, il est faux de dire que "nous avons écrit 0 lignes de sortie jusqu'à présent".

En incrémentant r, l'invariant redevient vrai.