Infections, Hoare triples, and debugging by printouts

car.c

public class Car {
  Seat[] seats;
  //...
  
  public int numEmptySeats() {
    int count = 0;
    int i;
    // { count = 0 }
    
    for(i = 0; i < this.seats.length; i++);
      // { 0 < i < this.seats.length }
    
      count += (this.seats[i] == null) ? 1 : 0;
      // { 0 <= count < this.seats.length }
    
    // { count is the number of elements of seats equal to null }
    return count;
  }
}


/*
DRILL
1. Had I not noticed the unwanted semicolon, I would want to monitor the value of `count` and therefore would add 
printouts within the for-loop, before the count incrementer. When I did not see the expected printouts,
I would know that code within the for-loop was not executing as I had expected.

2. See above.

3. The strategy I specified in response 1 would not inform me that the properties fail to hold because I have not 
specified a precondition that `this.seats.length` is greater than zero. If I were to add that precondition
and validate it via a printout, it would still not be informed that properties fail to hold because these properties
are logic concerns (level 3) and the defect occurs on level 2.

4. An infections is an erroneous piece of program state. The infection begins on line 9 because the intended program state
is to increment `i`, but the actual program never does so.

5. Hoare triples allow you to make pre and post conditions of a command explicit. They represent the "intended program state"
as defined by an infection. Debugging by printouts allow you to evaluate the "actual program state" in order to understand if
pre or post conditions are not met, suggesting an infection.
*/

" it would still not be informed that properties fail to hold because these properties
are logic concerns (level 3) and the defect occurs on level 2."

Not so.

Level 1: "This execution is correct"
Level 2: "All executions of this code are correct"
Level 3: "If module A is linked with any module B that satisfies a certain specification, then all executions of the combined program will be correct."

Level 3 correctness is strictly stronger than level 2 correctness, which is strictly stronger than level 1 correctness. An actual failing execution shows that there is a flaw in the logic of the program.