Lecture Notes for Advanced Programming II

30 January 2003 - Program Correctness

Understanding Programs

• Straight-line programs are easy to understand.

  • Begin at the beginning, read to the end, stop.

• if and case statements make understanding tricker.

  • Nested if and case statements make understanding exponentially trickier.

  • Consequently, avoid deeply nested statements.

Understanding Loops

• Understanding loopy code is harder than understanding straight-line code.

• How many times does the loop execute?

• When does the loop stop executing?

Loop Invariants

• The trick is to find something about the loop that's always true.

  • Always true - before, during, and after.

  • It's easier to verify something stays true.

    • Once through the loop does it.

    • As long as you don't have too many case or if statements.

Example

• Search for an element in a vector

• The invariant must be true before the loop executes

• It must be true after the guard executes

• It must be true at the end of the loop body

• It will be true after the loop exits

• The combination of the invariant and negated loop guard gives what we want.

Assertions

• Assertions are part of the C standard library.

• Defined in <cassert> for C++.

• Defines the assert() macro.

The assert() Macro

• The assert() macro takes a single expression as an argument.

  • If the expression is true, nothing happens.

  • If the expression is false, the macro blows up.

  $ cat t.cc
  #include <cassert>
  
  int main() {
    const int two = 2;
    assert(two < 1);
    }
  
  $ g++ -o t t.cc
  
  $ ./t
  Assertion failed: two < 1, file t.cc, line 5
  Abort(coredump)
  
  $ 
  

• Failed assertions create a core file for your debugging pleasure.

Programming with Assertions

• If you make an assumption, check it with an assertion.

• "Oh, input will always have at least one character."

  • Wrong:

    std::string inp;
    std::cin >> inp;
    if (inp[0] == '#') { ... }
    

  • Right:

    std::string inp;
    std::cin >> inp;
    assert(inp.size() > 0);
    if (inp[0] == '#') { ... }
    

  • If your assumption is ever wrong, it will be obviously so.

• Don't forget to document your assumption.

  // Input is never empty.
  
  assert(inp.size() > 0);
  

Disabling Assertions

• Assertions can be turned off by defining NDEBUG.

  • Either on the command line

    g++ -DNDEBUG ...
    

    or in your code (before the <cassert>).

    #define NDEBUG
    #include <cassert>
    

• Do not put side-effecting expressions in assert macros.

  • Disabled assertions don't execute their expressions.

    Wrong:

    // The file must exist, I just created it.
    assert(ifs.open(fname));
    

    Right:

    // The file must exist, I just created it.
    const bool ok = ifs.open(fname);
    assert(ok);
    

• Always run with assertions enabled.

This page last modified on 31 January 2003.