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

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

2 Answers 2

Reset to default
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.

Improve this answer
$\endgroup$
4
  • $\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, 2015 at 2:13
  • $\begingroup$ @AndrewRaleigh I've added some details $\endgroup$
    – Klaus Draeger
    Nov 9, 2015 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, 2015 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, 2015 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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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