Что такое инвариант цикла в следующем коде

Question

Что такое инвариант (ы) цикла в этом примере кода?
Это фрагмент кода, реализованный на языке программирования C:

//pre-condition m,n >= 0
x=m;
y=n;
z=0;
while(x!=0){
  if(x%2==0){
    x=x/2;
    y=2*y;
  }
  else{
    x=x-1;
    z=z+y;
  }
}//post-condition z=mn

Вот мои первоначальные ответы (Loop Invariant):

1. y>=n
2. x<=m
3. z>=0

Я все еще не уверен в этом. Благодарю.

Answer 1

Ваши ответы действительно инвариантны, но мало говорят об условиях вашего цикла. Вы всегда должны искать конкретные инварианты. В этом случае это довольно просто, поскольку внутри вашего цикла есть только две (эксклюзивные) операции.

Первый x' = x/2; y' = 2*y; выглядит как инвариант x*y,

Второй x' = x-1; z' = z+y; не является: x'*y' = x*y - y, Но если вы добавите z опять это будет инвариантным. z'+x'*y' = z + y + x*y - y = z+x*y,

К счастью, также первое условие инвариантно относительно z+x*y и, таким образом, мы нашли инвариант цикла.

• Предварительное условие: z+x*y = m*n
• Постусловие: x=0 (условие цикла) и, следовательно, мы можем вывести из нашего инварианта: z = m*n