Defensive Programming

Assert Invariants

An invariant is a condition the program expects to remain true after an operation.

invariant Programs can report an invariant check without intentionally stopping execution.

Assert Invariants

withdrawal
assert_invariants.cpp
Replay: real traced execution (multi-file project)
#include <iostream>

int main() {
    int balance = 20;
    int withdrawal = 10;

    int nextBalance = balance - withdrawal;
    bool invariantHolds = balance >= 0 && withdrawal >= 0 && nextBalance >= 0;

    std::cout << "balance=" << balance << std::endl;
    std::cout << "withdrawal=" << withdrawal << std::endl;
    std::cout << "nextBalance=" << nextBalance << std::endl;
    std::cout << "invariantHolds=" << invariantHolds << std::endl;
    return 0;
}

#include <iostream>

int main() {
    int balance = 20;
    int withdrawal = 5;

    int nextBalance = balance - withdrawal;
    bool invariantHolds = balance >= 0 && withdrawal >= 0 && nextBalance >= 0;

    std::cout << "balance=" << balance << std::endl;
    std::cout << "withdrawal=" << withdrawal << std::endl;
    std::cout << "nextBalance=" << nextBalance << std::endl;
    std::cout << "invariantHolds=" << invariantHolds << std::endl;
    return 0;
}

#include <iostream>

int main() {
    int balance = 20;
    int withdrawal = 30;

    int nextBalance = balance - withdrawal;
    bool invariantHolds = balance >= 0 && withdrawal >= 0 && nextBalance >= 0;

    std::cout << "balance=" << balance << std::endl;
    std::cout << "withdrawal=" << withdrawal << std::endl;
    std::cout << "nextBalance=" << nextBalance << std::endl;
    std::cout << "invariantHolds=" << invariantHolds << std::endl;
    return 0;
}

  1. balance ← 20, withdrawal ← 10, nextBalance ← 10, invariantHolds ← 1

    3int main() {4    int balance→ 20 = 20;5    int withdrawal→ 10 = 10; //@withdrawal=5, 3067    int nextBalance→ 10 = balance20 - withdrawal10;8    bool invariantHolds→ 1 = balance20 >= 0 && withdrawal10 >= 0 && nextBalance10 >= 0;910    std::cout << "balance=" << balance20 << std::endl;11    std::cout << "withdrawal=" << withdrawal10 << std::endl;12    std::cout << "nextBalance=" << nextBalance10 << std::endl;13    std::cout << "invariantHolds=" << invariantHolds1 << std::endl;14    return 0;15}
    outputbalance=20
withdrawal=10
nextBalance=10
invariantHolds=1

  1. balance ← 20, withdrawal ← 5, nextBalance ← 15, invariantHolds ← 1

    3int main() {4    int balance→ 20 = 20;5    int withdrawal→ 5 = 5;67    int nextBalance→ 15 = balance20 - withdrawal5;8    bool invariantHolds→ 1 = balance20 >= 0 && withdrawal5 >= 0 && nextBalance15 >= 0;910    std::cout << "balance=" << balance20 << std::endl;11    std::cout << "withdrawal=" << withdrawal5 << std::endl;12    std::cout << "nextBalance=" << nextBalance15 << std::endl;13    std::cout << "invariantHolds=" << invariantHolds1 << std::endl;14    return 0;15}
    outputbalance=20
withdrawal=5
nextBalance=15
invariantHolds=1

  1. balance ← 20, withdrawal ← 30, nextBalance ← -10, invariantHolds ← 0

    3int main() {4    int balance→ 20 = 20;5    int withdrawal→ 30 = 30;67    int nextBalance→ -10 = balance20 - withdrawal30;8    bool invariantHolds→ 0 = balance20 >= 0 && withdrawal30 >= 0 && nextBalance-10 >= 0;910    std::cout << "balance=" << balance20 << std::endl;11    std::cout << "withdrawal=" << withdrawal30 << std::endl;12    std::cout << "nextBalance=" << nextBalance-10 << std::endl;13    std::cout << "invariantHolds=" << invariantHolds0 << std::endl;14    return 0;15}
    outputbalance=20
withdrawal=30
nextBalance=-10
invariantHolds=0