Comment by eliteraspberrie

Here's an example in a getline implementation: https://github.com/eliteraspberries/ttyprompt/blob/master/ge...

        /*@ loop invariant i;
            loop invariant j >= 0;
            loop assigns j, eol;
         */
        for (j = 0; j < (size_t) i; j++) {
            if (read_buffer[j] == '\n') {
                eol = 1;
                j++;
                break;
            }
        }

Loop invariants are part of the ACSL specification language, and they can be verified automatically with Frama-C. http://frama-c.com/acsl.html