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

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?

• Hint: R is the loop invariant. Finding it is a creative step. If you have R, pack into P all that you know prior to the loop, verify the three conditions of the rule (by recursively annotating the loop body, in particular) and you are done. (If it doesn't work, your loop invariant is wrong. Try again.) So, what R have you tried? What does the program do? – Raphael Mar 10 '15 at 7:46
• Another hint: you can treat repeat-until loops as syntactic sugar and try to relate this rule to that for the while-loop. – Klaus Draeger Mar 10 '15 at 13:34
• P is the pre condition. Part of it is given as precondition of the whole program; you want to add the results of the first line. – Raphael Mar 10 '15 at 14:50

## 1 Answer

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).