Как найти петлю инвариант Java

Question

Я пытаюсь найти инвариант циклов (например, в следующем коде), я действительно не знаю, как найти инвариант в целом. Может ли кто-нибудь помочь мне с тем, как найти инвариант, а также помочь мне найти его для следующего кода? Спасибо

public static int div(int a, int b)
{
   int q = 0;
   while(a >= b)
   {
      a -= b;
      q++;
   }

   return q;
}

Answer 1

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

Например, q >= 0 является инвариантом цикла. Если вы хотите доказать, что функция возвращает положительное число, это все, что вам нужно. Если вы хотите доказать что-то более сложное, вам нужен другой инвариант.

Поскольку параметры в Java передаются по значению, а программа изменяет значения параметра aдавайте использовать a0 обозначить начальные значения a параметр. Теперь вы можете написать следующее инвариантное выражение:

a == a0 - (b * q)

Вы придете с этим инвариантом, наблюдая, что каждый раз, когда q увеличена, a также уменьшается на b, Так a0 уменьшается на b именно так q раз на каждой итерации цикла.

Этот инвариант может быть использован, чтобы доказать, что цикл производит q == a0 / bи что конечное значение a равно a0 % b,

Answer 2

Инвариант цикла - это некоторое условие, которое выполняется для каждой итерации цикла.

В вашем цикле предикат q >= 0 является инвариантом цикла, потому что это всегда верно. Необходимость анализа инвариантов цикла заключается в том, что при выходе из цикла могут быть гарантированы как инвариант цикла, так и условие завершения цикла. Так что в вашем случае при выходе из цикла мы можем быть уверены, что q >= 0 а также a < b,

Answer 3

Инвариант цикла - это некоторое условие, которое выполняется для каждой итерации цикла.

в вашем случае один инвариант:

q> = 0