7
$\begingroup$

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$$

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

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Andrew Raleigh Nov 9 '15 at 2:13
  • $\begingroup$ @AndrewRaleigh I've added some details $\endgroup$ – Klaus Draeger Nov 9 '15 at 9:47
  • $\begingroup$ 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. $\endgroup$ – Andrew Raleigh Nov 9 '15 at 14:53
  • 1
    $\begingroup$ 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). $\endgroup$ – Klaus Draeger Nov 10 '15 at 0:25
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.