# 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). Nov 22, 2015 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? Nov 9, 2015 at 2:13
• @AndrewRaleigh I've added some details Nov 9, 2015 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. Nov 9, 2015 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). Nov 10, 2015 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.