Inner loop construction from the compiler presentation

Hello,

what exactly is the point of the inner loop on page 34 of the compiler presentation? I first thought it was desugaring but it doesn’t seem to be the case. Essentially what happens is that this:

while (e)_Invariant(i)_Term(t;k) s

is turned into:

while (e)_Invariant(i)_Term(t;k) {
    while (0)_Invariant(e && i && 0 <= t <= k + 1)_Term(0) {}
    s
}

If I define:

inner(e) = while (0)_Invariant(e)_Term(0) {}

I get:

pc inner(e) q = e
vc inner(e) q = e => q

and using this I can verify (via calculation) that the program transformation didn’t change pc and vc. So what was the point?

It does. Your pc and vc also include that 0 \leq t \leq k + 1, since we’re doing total correctness (as explained on the slides…)

Try writing down all vc/pc expansion to see what is going on.

I might have made a mistake in the calculation. But we already check everything if we apply pc and vc to the original program, right? So why make things more complicated?

Well, we could have chosen a more complicated example, where you actually need two loops, but that would not have made understanding the problem any easier.

The question is why I would actually need two loops in the first place? From my understanding pc and vc prove total correctness in the presence of a “good” invariant and termination term.

Also why is none of this actually in the lecture notes?

Well, sometimes you just do. And we should be able to show total correctness for these programs. But we are not, for the reasons explained in the presentations. Please watch the recording if you have not done so already.

As explained in the project presentation video, the problem is easy to avoid on paper. Since the lecture notes are only about the “on paper” part, they ignore this. The project description briefly mentions it.

I misunderstood the slides. The inner loop is not some clever trick meant to help us verify the program, rather you wanted to show how to handle nested loops, so you added the simplest possible nested loop into the existing one and then showed the problem that arises with invariants needing to know about the k.

1 Like

Yes, that was my intention.