Control Flow

Loop Invariant

A loop invariant is a fact that stays meaningful before and after each iteration.

invariant `total` is always the sum of the values processed so far.
processed count `processed` records how many values have contributed to the invariant.

Loop Invariant

limit
loop_invariant.c
Replay: real traced execution (multi-file project)
#include <stdio.h>

int main(void) {
    int limit = 4;
    int total = 0;
    int processed = 0;

    while (processed < limit) {
        processed++;
        total += processed;
    }

    printf("processed=%d\n", processed);
    printf("total=%d\n", total);
    return 0;
}

#include <stdio.h>

int main(void) {
    int limit = 3;
    int total = 0;
    int processed = 0;

    while (processed < limit) {
        processed++;
        total += processed;
    }

    printf("processed=%d\n", processed);
    printf("total=%d\n", total);
    return 0;
}

#include <stdio.h>

int main(void) {
    int limit = 5;
    int total = 0;
    int processed = 0;

    while (processed < limit) {
        processed++;
        total += processed;
    }

    printf("processed=%d\n", processed);
    printf("total=%d\n", total);
    return 0;
}

  1. limit ← 4, total ← 0, processed ← 0

    3int main(void) {4    int limit→ 4 = 4; //@limit=3, 55    int total→ 0 = 0;6    int processed→ 0 = 0;

  2. processed ← 1, total ← 1

    pass 1 of 4
    8while (processed0 < limit4) {9    processed→ 1++;10    total→ 1 += processed1;11}
    All 4 passes — pass 1 is the card above
    passprocessedtotal
    10 → 10 → 1
    21 → 21 → 3
    32 → 33 → 6
    43 → 46 → 10

  3. printf("processed=%d ", processed);

    13    printf("processed=%d\n", processed4);14    printf("total=%d\n", total10);15    return 0;16}
    outputprocessed=4
total=10

  1. limit ← 3, total ← 0, processed ← 0

    3int main(void) {4    int limit→ 3 = 3;5    int total→ 0 = 0;6    int processed→ 0 = 0;

  2. processed ← 1, total ← 1

    pass 1 of 3
    8while (processed0 < limit3) {9    processed→ 1++;10    total→ 1 += processed1;11}
    All 3 passes — pass 1 is the card above
    passprocessedtotal
    10 → 10 → 1
    21 → 21 → 3
    32 → 33 → 6

  3. printf("processed=%d ", processed);

    13    printf("processed=%d\n", processed3);14    printf("total=%d\n", total6);15    return 0;16}
    outputprocessed=3
total=6

  1. limit ← 5, total ← 0, processed ← 0

    3int main(void) {4    int limit→ 5 = 5;5    int total→ 0 = 0;6    int processed→ 0 = 0;

  2. processed ← 1, total ← 1

    pass 1 of 5
    8while (processed0 < limit5) {9    processed→ 1++;10    total→ 1 += processed1;11}
    All 5 passes — pass 1 is the card above
    passprocessedtotal
    10 → 10 → 1
    21 → 21 → 3
    32 → 33 → 6
    43 → 46 → 10
    54 → 510 → 15

  3. printf("processed=%d ", processed);

    13    printf("processed=%d\n", processed5);14    printf("total=%d\n", total15);15    return 0;16}
    outputprocessed=5
total=15