Video 0-6: §0.4 Correctness proofs (part 2): example

0:03 so let's see an example of such a proof on on this code which finds the maximum of an array in the obvious way you step through it and you keep track of a maximum of a prefix of the array

0:18 that's intuitively what the code does for a formal proof we have to find a loop invariant so I've already done that job for you and the loop invariant consists of two parts and will be useful to give them colors I hope that these are distinguishable no matter what kind of limited color side you might have so this is a little a little lighter than the other one right uh it's red and blue in case case that helps

0:52 so the first thing we have to check we have to go through these three conditions and show that each is satisfied with the loop condition that we've chosen the first condition says the loop condition holds before the loop so I marked in the code these four positions a to d uh so let's have a look at at this first part um

1:19 if we look at position a uh we've just initialized things so that I is one so if you look at what the loop invariant really says here I'm just copying this and insert what the value of I at this point is

1:41 I mean this this takes a lot longer to write than to Think Through uh if you put I minus 1 here so this is just 0 up to zero it's the set with just the zero in it

1:58 well the second bit is not very interesting if we insert one here uh that's something that we assumed in the loop so we call the function with an array that has at least one element and so that part is what guarantees this first bit I should have done this in red I guess sorry light blue okay I'm not that colorblind but

2:32 so that that guarantees the first bit of the loop invariant just by assuming it at the beginning of the function and that's something you often have to do now for the second bits we we can just rewrite this so the second bits

2:50 that maximum doesn't really do anything right it's just insert this it takes the maximum over a set that contains a single value so the maximum will always be that single value

3:09 on the right is really just a of zero so the this the claim that we're making is current Max is the value of a of zero and that's exactly how we've assigned it just before that so that that's also fine okay uh so that was that was the somewhat easy bit because it didn't really involve the loop yet

3:40 I'll try to have the code on the slide as well as my writing so I'm gonna be a bit of a challenge for the second part we need to show that the loop invariant and the condition of the loop so that's this fact that I is strictly less than n these two things together at B guarantee that we have again the loop invariant at C so that's an implication right we talked about last time at length how you can prove how you can possibly prove implications we talked about these all these different proof templates and so on so that's applicable here now in this case the most convenient bit is to do a case distinction first

4:39 and the reason for that is that inside the loop there's an if so there's really two things that can happen depending on whether the if is taken or not so it's quite natural that we want a case distinction based on whether or not this this Loop condition is this this if condition is true

5:02 have a look at those two cases separately so a first case would be that um this is this is true intuitively that we found a new minimum a new maximum right so the the new element we're looking at we're taking into account now is bigger than what we currently had as the maximum foreign

5:50 we use what we had in the premise we're proving an implication so we can assume what's on the left side of this implication Arrow in particular we know that at the position B in the code here the invariant I was true and conveniently that's just after where we just just before where we are in the code now if we're looking at this if so using the the red part of the loop invariant we can we can use what we know about current Max

6:27 namely that current Max solve bar is of this expression like just up to I minus 1. if we're in this case then the if statement is true in the the then branch is executed so we assign current Max

7:13 now what does that mean for this this red statement of the loop invariant we can already have a look at that uh let's start with the maximum what that means is I can now extend the range of this maximum in the Lubin variant for one more index and it will still be true because we've seen the current maximum so the maximum of the elements up to position I minus one that was current Max but AI was even bigger so clearly AI is the maximum of everything up to position I it's just rephrasing this again foreign

8:06 this is almost like the next Loop invariant that we need except that we're not yet at positions C instead we've only executed line 9 so far so what happens in line 10 is a is something that changes the value of I we make I want bigger so that means in the loop invariant we have to adjust the value of I if this was true before then if we now make i1 bigger we have to make it in the statement one smaller to compensate for that so this again this is true at after line nine

8:55 and so once we said I to I plus 1 with uh an i minus one because this is now actually one one bigger okay and now if you look at this that is exactly the red part of the loop invariant uh carrying it by character the same thing

9:39 and also after line 10 I mean should have stressed this that's really at C it's the same same position so that in that case so we're that's that's often how proof goes so zoom out a bit right uh we're in we're proving the second part of of our overall claim and within that K in that claim we're in the first case of a case distinction and within that case we've proven that the red part of the loop invariant holds again at the bottom of the loop body so next the blue part uh what can we say about the blue part

10:26 we now add B that the loop invariant was true but we know more we also know that the condition was true so the loop condition otherwise you would have left the loop so at this point I was strictly less than n the Lubin variant only says less or equals was strictly less is stronger

10:47 um I don't know I'll I'll mark this with red and then Mark this with blue I don't want to write it in blue because the contrast is not that not that great

11:16 and uh actually no matter what happens in the if statement that doesn't touch I but we always increment I afterwards so by the time we get to C will have made I one bigger so we can only say that I minus 1 is less than n but that still implies that I is less or equal n because it's integers

11:50 and so that that finishes the blue part and I think we can move this outside of the case distinction because it's the same for both cases so I'll move I'll move this down here and out of the case distinction

12:19 which was that the the if statement is false right this one in that case we don't execute the if statement right but we still have to argue for the the red part to be true at the end of the loop

12:55 so we don't touch current Max however we know something we know that the previous maximum is at least as big at this next as this next element so we can again extend the range of the maximum by one more element

13:15 if we take our maximum and go from zero up to including I then that is still the value of current maximum we haven't changed it is fine if we have this tie effect the next element is another occurrence of the maximum so it's fine we can still pick the first one

13:37 and the rest is really by the same arguments so this is and so after we incremented c i we do the same step at C okay notice that we're basically following the structure of the code but we're also following the definition of a maximum it's either if you if you add one more element either that element is a new maximum or it's not that's that's all that happens

14:32 so that finishes the the proof of the red claim in both cases of the case distinction and we could get rid of the case distinction for the the blue part because it behaves the same in both ways

14:58 uh that proves that I hold at position C at the end of the loop buddy okay and that was that was this part so that finishes I could have ticked this off we've done that here done that now what's left is uh the Roman third which is that the loop condition actually does what we want for the Post statement for the Post condition

15:39 and for that uh it's basically sufficient to to spell out what that is and I'll spare you another round of me typing this copying it so that's the two bits of I but then we also have not the condition the condition was that I is strictly less than n so not the condition is I greater equal n

16:20 Mark that here okay you remember and so if you look at this uh or copy the wrong thing here this was from condition zero ah there's no point if you can't read it right

17:03 so if we're at this point then we take the last two conditions uh okay again shouldn't have copied this this was an eye I inserted the the one there these two things together obviously mean that I is equal to n

17:22 and then if you insert n in here you get the statement that uh current Max is the same as taking the max over the entire array because we're letting K go from 0 up to n minus one

17:44 foreign so this is true at the end of the of the code intuitively that's what we wanted because that's the maximum of the array okay