Probleme – Un compteur de lignes, de mots et d'octets, qui se chaîne

1. La fonction. La seule difficulté est la définition d'un mot : une suite maximale de caractères non blancs. On la traduit par un booléen d'état, et l'invariant le dit.

/* Compte les lignes, les mots et les octets lus sur f jusqu'a la fin du flux.
   Un mot est une suite maximale de caracteres non blancs.
   Preconditions  : f ouvert en lecture, les trois pointeurs non nuls et distincts.
   Postcondition  : f a ete lu jusqu'a la fin ; il n'est PAS ferme (l'appelant
                    decide, car f peut etre stdin). */
void compter(FILE* f, int* lignes, int* mots, int* octets) {
    assert(f != NULL && lignes != NULL && mots != NULL && octets != NULL);
    *lignes = 0; *mots = 0; *octets = 0;
    bool dans_mot = false;
    int c = fgetc(f);
    /* INVARIANT : *octets, *lignes et *mots comptent respectivement les
       octets, les '\n' et les mots COMPLETEMENT COMMENCES dans le prefixe
       deja lu ; dans_mot dit si le dernier octet lu etait non blanc. */
    while (c != EOF) {
        *octets = *octets + 1;
        if (c == '\n') { *lignes = *lignes + 1; }
        bool blanc = (c == ' ' || c == '\n' || c == '\t');
        if (!blanc && !dans_mot) { *mots = *mots + 1; dans_mot = true; }
        if (blanc) { dans_mot = false; }
        c = fgetc(f);
    }
}

2. Preuve et coût.

Terminaison. Variant : le nombre d'octets restants dans le flux. Chaque tour en consomme exactement un par fgetc, et la boucle s'arrête sur EOF. Sur un flux fini, elle fait donc exactement autant de tours qu'il y a d'octets.

Correction. L'invariant tient à l'entrée : le préfixe lu est vide, les trois compteurs sont nuls, dans_mot est faux. Il se conserve : un octet lu incrémente <em>octets ; un ' n' incrémente </em>lignes ; et <em>mots n'augmente qu'au passage* blanc $\to$ non blanc, c'est-à-dire une fois par suite maximale de non-blancs, ce qui est la définition d'un mot. À la sortie, le préfixe lu est le flux entier : les compteurs sont ceux du flux.

Le cas limite qui décide de l'écriture. C'est dans_mot initialisé à false : sans quoi un fichier commençant par une lettre ne compterait pas son premier mot. Et c'est bien la seule initialisation qui rende l'invariant vrai avant le premier tour — l'invariant impose le code, il ne le commente pas.

Complexité. $\Theta (m)$ en temps pour $m$ octets, $\Theta (1)$ en mémoire. Mesure sur un fichier de $62$ octets : 4 15 62, identique à ce que rend wc du système.

3. Lire stdin. La fonction prend un FILE* et le main lui passe stdin. On y gagne exactement trois choses, et elles sont mesurables :

La composition. ./generer | ./wc fonctionne sans qu'aucun fichier n'existe. Un programme qui ouvrirait "entree.txt" ne se brancherait sur rien.

Le choix laissé à l'appelant. La redirection ./wc < donnees.txt donne le comportement « fichier » sans une ligne de code de plus. C'est le shell qui ouvre, et il sait le faire mieux que nous — droits, chemins relatifs, messages d'erreur.

L'absence de mémoire. Rien n'est stocké : le programme traite un flux de n'importe quelle taille dans une mémoire constante. C'est ce que la boucle sur fgetc garantit et qu'un malloc de la taille du fichier détruirait.

Le point de discipline. La fonction ne ferme pas f. Fermer stdin au milieu d'un programme serait une faute, et la fonction ne sait pas ce qu'elle a reçu. Qui ouvre ferme — c'est le pendant exact de « qui alloue documente qui libère ».