Skip to content

Instantly share code, notes, and snippets.

@bbuchalter
Created March 2, 2018 17:15
Show Gist options
  • Save bbuchalter/4b7e96f5a736d5ead8179aaa9e920ca3 to your computer and use it in GitHub Desktop.
Save bbuchalter/4b7e96f5a736d5ead8179aaa9e920ca3 to your computer and use it in GitHub Desktop.
Infections, Hoare triples, and debugging by printouts
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.
*/
@jkoppel
Copy link

jkoppel commented Mar 2, 2018

Hello! You're the first person in the course to attempt this. Thanks for taking the risk. (I've used this example in my 1-on-1 coaching, where I could actually talk over it with someone.)

The main problem is that the assertions you wrote are too weak. "count is the number of elements of seats equal to null" does not follow from "0 <= count < this.seats.length." As a result....of course your properties are not violated. Doing it correctly requires writing a loop invariant. The reason I made this optional is that I'm loop invariants are not required for this course (they were in the appendix of the Hoare logic handout, and not particularly thoroughly explained). I'll update the exercise page to emphasize this.

Without having correct assertions that are indeed violated by the buggy program, you can't really do the rest of the exercise. You said some things that look correct, but I want you to actually fully understand this example.

@jkoppel
Copy link

jkoppel commented Mar 2, 2018

" 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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment