Finding a Hoare logic correctness proof for a Repeat-Until loop

Question

How can we prove a program in repeat until using Hoare Logic?

I've found a rule like this:

{P} S {R}, {R ^ ~B -> P}, {R ^ B -> Q}

for

{P} 
repeat 
  S 
until B 
{Q}

But I still can't find any explanatiom how I can use this rule

For example in this question:

{x > 0 ^ y > 0}
     z:=0; u:=x; 
     REPEAT
        z:=z+y;
        u:=u-1;
     UNTIL u=0;
{z = x * y}

How I can use the rule to prove this program?

UPDATE I've tried to find invariant loop:

R : Z = X*Y + (Y - Y*U)

But I still confuse what is P?

Answer 1

Note that the loop is not the outermost construct in your program; that is a sequential composition. In order to apply this rule, you first need to take care of the initial assignments. In this case that is straightforward: you get that the formula $x>0\wedge y>0\wedge z=0\wedge u=x$ holds after $z:=0; \ u:=x$.

For the loop rule, you need three formulas: a precondition $P$, a postcondition $Q$, and an invariant $R$, satisfying the premises of the rule. The precondition $P$ also needs to follow from the formula we obtained above. The postcondition $Q\equiv z=x*y$ is already given in your initial triple. What is left to do is therefore to find $P$ and $R$ such that

• $(x>0\wedge y>0\wedge z=0\wedge u=x)\to P$,
• $\{P\}\ z:=z+y;\ x:=x-1\ \{R\}$,
• $(R\wedge u\neq 0)\to P$,
• $(R\wedge u=0)\to z=x*y$.

A special case which may be worth trying here is to assume that the third condition holds with equality, i.e. $P\equiv (R\wedge u\neq 0)$. This reduces the problem to finding $R$ such that

• $(x>0\wedge y>0\wedge z=0\wedge u=x)\to (R\wedge u\neq 0)$,
• $\{R\wedge u\neq 0\}\ z:=z+y;\ x:=x-1\ \{R\}$,
• $(R\wedge u=0)\to z=x*y$,

which is essentially an application of the usual while rule. As for how to find $R$, that is in general a very tricky problem. You seem to be looking in the right direction, but you invariant still needs some work (checking which of the conditions it fails, and how, may help with that).