Got it! This site uses cookies. You consent to this by clicking on "Got it!" or by continuing to use this website.nbsp; Note: This appears on each machine/browser from which this site is accessed.
Let us show some code that initializes an entire array from 1 to n to the value of 0 (zero).
Here is the C code.
Note: There is no output in this program.
//
//
int i = 0;
//
int n = 10;
// inv:{ a[0..i-1] = 0 }
while (i != n) {
//
//
//
//
a[i] = 0;
//
//
i = i + 1;
//
}
//
//
//
// post: { a[0..n-1] = 0 }
3. Example 1
int i = 0;
int n = 10;
while (i != n) {
a[i] = 0;
i = i + 1;
}
4. Correctness
The above has shown partial correctness - when the loop stops the goal is reached.
To informally show total correctness one observes (the math gets more involved) that progress is made towards the goal during each loop body iteration so that eventually the loop will stop.
Notice that we did not use n in the above partial correctness proof. The value of n is needed in the total correctness part of the proof.
