Relating Rosen's program-proofs to lectures loop-proofs

Date: Mon, 29 Mar 2004 12:17:14 -0600 (CST)
From: Ian Barland 
Newsgroups: rice.owlnews.comp280
Subject: Re: loop invariant/goal

> I have a question about the difference between a loop invariant and a goal,
> especially in terms of what Rosen calls initial and final assertions.  ...

The short answer: Show that if the initial assertions are true when you start executing the block of code, then the final assertions are true when you finish.

The long (but not complicated) answer, which highlights parts of the reading in Rosen (and how the specific topic of loops relates to the rest of the reading):

• In lecture, we focused on proofs about loops. In Rosen he's talking about not just loops, but about an entire (imperative) language with assignment, if statements, and sequencing (block-statements) as well. I specifically left to the reading alone, discussion of everything-but-loops.
• Turning now to the specific hw question in Rosen, we see he's not quite asking about a loop, but rather about a sequence-of-(three)-statements (the third of which happens to be a loop). He tells you what you can assume coming in to that block of three statements, and what you need to prove upon exit.

• What does that mean for us? A quick glance shows the first two (assignment) statements should be easy enough; clearly it'll be the loop that will be the bulk of the work.

  You'll have to figure out what you want to attempt as the loop invariant, L.

  What about the loop goal, G? What should be true when finishing the loop? Well, for this exercise, this is more or less dictated to us: Rosen specifies what to prove true when the entire sequence-of-three statements finishes, which coincides with the end-of-loop.

  (Were there a few more statements after the loop, we'd instead use the loop-goal plus the actions of those further statements, to try to show what will be true at the end of the entire sequence.)

• So what part do the "initial assertions" play? These are things you know at the start of all three sequential statements. Presumably you'll use them (plus knowledge of what the first two statements do) to help show that your loop invariant is true initially.
• What do you need to write on your homework? I'm mostly looking for the proof about the loop (and its four proof obligations mentioned in lecture).

• In the sub-step of showing that your loop invariant is true initially, when going from what's true when the block-of-three-statements starts to what's true when the loop starts, do you need to spell things out in full detail, like Rosen gives in the reading? No. Do give a half-sentence nod to the fact that some deduction is going on: something along the lines "Because x,y are integers with y=5, clearly after

        x := a
        y := b+17
  

  we know that a,b are integers with b=22." But in the continuing trend of our proofs being less low-level as the semester progresses, you don't need to go through and write -- as shown in the reading -- {phi,psi} x := a {phi',psi'} [where phi etc are formulas] and then cite the inference rule for assignment to show that knowing formulas {phi, psi} plus the semantices of x:=a is enough to prove the formulas {phi',psi'}, and likewise again for the second statement.

  (Though, if you go on to study programming languages, you will see that full notation. If you pick up a paper proposing new constructs to a language (e.g. adding generic types to Java), you will see formal definitions of the semantics and type-inference-rules for the proposed language.)

Whew!