SE450: DBC: Common assertion usage [8/24]

Internal Invariants
replace

if(i == 0) {
 ...
} else if(i == 1) {
 ...
} else { // i == 2
 ...
}

with

if(i == 0) {
 ...
} else if(i == 1) {
 ...
} else { 
 assert i == 2;
 ...
}

Control Flow Invariants
replace

switch(value) {
 case command2.A:
  ...
  break;
 case Foo.B:
  ...
  break;
}

switch(value) {
 case Foo.A:
  ...
  break;
 case Foo.B:
  ...
  break;
 default:
  assert false;
}

Place assert false; in code you think will not be reached. You'll find out if it is!

Never allow assertion code to have side affects, since assertions can be disabled. Example:

  assert i++ == 3;