# Loop variant for a while loop that occasionally doesn't decrease?

I'm working on practice problems for a test I have, and every example of loop variant decreased with every iteration of the loop. On this one, the values remain the same when a < b. My attempts also got me a loop variant that has a chance of a negative since occasionally a becomes larger than b and vice versa. Any advice on attempting to find and prove the loop variant for this question?

def mystery(a,b):
# Precondition: a >= 0 and b >= 0
while a >= 0 and b >= 0:
if a < b:
a, b = b, a
else:
a = a - 1
return a


EDIT: For anyone who is interested in this question, my best solution is as follows.

$$f_{1} = a + 2b + 1$$

• Very nice! I think you should make it an answer (or even the answer). – Anton Trunov Nov 22 '15 at 15:05

Just a hint for now, since this is a practice problem: consider a lexicographic combination of orders.

In some more detail: Suppose you have two maps $f_1:S\to D_1$ and $f_2:S\to D_2$ from your program states $S$ into well-founded ordered domains $(D_1,\le_1)$ and $(D_2,\le_2)$. The lexicographic combination of $\le_1$ and $\le_2$ is the order $\le$ on $D_1\times D_2$ given by $(x_1,y_1)\le(x_2,y_2)$ iff either $x_1\le_1x_2$, or $x_1=x_2,y_1\le_2y_2$. It is also well-founded.

So if $f_1,f_2$ are such that

• $f_1$ never increases, and
• whenever $f_1$ does not decrease, $f_2$ does,

then the map $(f_1,f_2):S\to D_1\times D_2$ is a variant proving termination.

• Thanks for the hint! We haven't done lexicographic combinations, I'll look into it now. Could you explain how that would allow it to decrease in all cases? – Andrew Raleigh Nov 9 '15 at 2:13
• @AndrewRaleigh I've added some details – Klaus Draeger Nov 9 '15 at 9:47
• That makes a lot of sense, never thought of it that way. In this case, would $$f_{1} = a$$ and $$f_{2} = b - a$$? Although it occasionally remains the same, and the lecture slides don't say anything about that being allowed or not. – Andrew Raleigh Nov 9 '15 at 14:53
• The problem with $f_1=a$ is that it may increase (when $a,b$ are swapped). Try to find an expression which remains the same in this case, and decreases in the other one (when $a$ is decremented). – Klaus Draeger Nov 10 '15 at 0:25

Here is an approach involving only one mapping: $$f = (a+1) \cdot (b+1) + (b - a)$$ Simple case analysis can show that $f$ always decreases as you go through the loop.