I shoot photos of my teaching boards since a while. I like it quite much, and I see several advantages. First of all, even if I tend to over-preparate my teaching interventions, I always say a bit more in live than what was planned. Questions for example force me to improve my explanations, add some details, or let me remember of something I forgot to write during the preparation. Afterward, I try to remember what I've added to improve the things for the next years, but the loss of information is always too high.

Another reason is that it forces me to improve my style on the board. Keep readable, organize (geo)graphically concepts, and so on. My students appreciate (or should

Anyway. I assume that some board pictures are not enough to completely replace 2 hours of blahblah which came with it, but that's all what I have. And yes, I do 2 hours of lecture on 3 or 4 boards only...

This is the third lecture on C, about static memory. I distribute the source code of a program during that course, and we predict its output.

This is the fourth lecture of C. It was a set of exercices on pointers (without any sheet given to the students).

Fifth lecture of C, on dynamic memory.

I gave this lecture twice since I had 2 groups in C this year. This is what I told to the first group. That's maybe not as organized as with the second group, but I seem to remember that I said something to the first group that I forgot for the second one. Of course, I can't remember of what it was....

Actually, I regret that I didn't had that idea earlier...

And this is a practical comming from the TOP lecture, about proofs. That was not an easy practical, since the algorithm to proove was plainly wrong, and since I didn't notice before comming to the practical (even if I'm the one writing the sheets)...

In that case, the board pictures are really not enough, I admit, but that's all what I have. The sheet is available here. Let me give some details about the content, since not all groups managed to find the time to do that exercise. Shame, it was funny.

Moreover, some students asked for a correction. I also distributed the teacher of the sheet, even if I don't really feel confortable with doing so. Indeed, these documents are like the score intended to help my collegues to play the right music during the show, not really corrections helping the students to understand the answers. The difference is a meta level: these documents help my collegues helping students. But some of you may find it useful anyway.

The first board only shows how to guess the invariant: You must perfectly undersand the algorithm. Plus your invariant have some parts looking very close to the post-condition or you'll be unable to connect the end of the algorithm to the post-condition, plus some parts looking like the pre-condition that you feel plausible, or you'll be unable to connect the begining of the algo to the precondition at the end of your proof.

The proof goes as expected. I've a post-condition, and I traverse the code from the end to the beginning to compute the mandatory precondition. On the way, I encounter a while loop, so I apply the classical rule to get the proof obligations that I have to fullfil before stating that WP(while,post)=inv. As usual, the obligations 2 and 3 are very easy to show while the first one is really more difficult.

Indeed, there is a little bug on that board since if you want to get it working, you have to consider that the if branching of the code DO have a else branch (which is empty). Ie, read "if (cond) then (inst)" of the provided listing as "if (cond) then (inst) else (nothing)" before applying the rule dealing with if branches. It seems useless, but it changes the elements of the upcoming proof. Anyway, after some rewriting, you get that the right part of the implication constituting the first proof obligation is the mega expression at the bottom right of the first board, near the rounded K.

The begining of the third board is about concluding that the first proof obligation is fullfiled, then. We take each part of K one after the other, and show that it's true provided that the elements of the left expression are there. That's quite trivial actually. When you prooved that one element of the left is true, we strike it.

Under the horizontal rule of that third board, now that the last proof obligation surendered, we only have to finish stuff by simply computing the WP at the begining of the code. Easy stuff, we're almost here.

But that's where the world falls appart. It's impossible to propagate the computation of WPs. With the choosen invariant (which is mandatory for the wanted postcondition), we say that for each k in [1,2], f(k)>=m. But the initializations in the code only give it true for k=1, not for k=2...

Actually, the board already shows the traces of a try to fix things: We changed [1;2] into [1;2) (ie, the set {1,2} to the set using an open interval). But that impacts the loop invariant, which must be changed accordingly. That, in turn, changes the post-condition. So we just prooved that if the minimal element is on the last position, this code doesn't find it. Pity.

Looking again at the algorithm, you see imediately that the while condition is flawed. You must use i<=n and not i<n. With that modification, you can change your proof elements again, in the other direction. You take again the postcondition we're interested in, you get again the initial invariant we were looking at, and we manage to propoagate the WP computation until the first lines of the code this time.

At least I guess so because the students didn't allowed me to do it right so that I can take a picture of the fixed version of the board. They argued that it was friday, 5:59pm

The conclusion that I see in this is that proof is quite laborious I admit. But that method is more efficient to find bugs than the "we clearly see that" one. We looked at that code for one hour and half, and nobody saw the bug before the proof process.

The fourth picture is simply like the second and third one in the right orientation (but then, you have to read the right half before the left half).

EDIT: I translated that post because ikiwiki became allegic to french accents at some point. How, right, sorry. Did I mention that all that board are actually written in french because that's the language we use to teach in France? There is even a law forcing us to do so...