Инвариант петли (Java)

Question

У меня есть следующий код, чтобы перевернуть цифры в целое число:

public class integerReversal {
    public static int reverseNum(int number){
        int reversed = 0;
        int remainder;
        //{I:  ; B: number > 0}
        while (number > 0){
            remainder = number % 10;
            number = number / 10;
            reversed = reversed * 10 + remainder; 
        }
        //{I: ; !B: number == 0}
    return reversed;
    }
    public static void main (String [] args){ 
        System.out.println(reverseNum(1262015 ));
    }
}

Мой профессор поручил нам написать этот код, а также сказал написать инвариант цикла и условие цикла. Я понимаю условие цикла здесь, я просто не уверен, что я должен смотреть на инвариант. Я понимаю, что это некое условие, которое будет выполняться в начале и в конце цикла while, для каждой итерации я просто не вижу, что это будет здесь. Советы будут оценены.

Answer 1

В вашем случае обратное>=0 является вашим инвариантом цикла, так как оно всегда будет оставаться верным, независимо от того, нарушаете ли вы цикл или нет.

Answer 2

Инвариант цикла - это константное выражение, включающее значения, предназначенные для изменения каждой итерации.

В вашем случае в каждой итерации number это номер без самой правой цифры и reversed это число, которое вы построили из остатков в предыдущих итерациях. Поэтому я считаю, что ответ таков: на каждой итерации следующее выражение остается постоянным:

number * 10 + reverseNum(reversed)

Другими словами, в любой момент вы можете вернуть исходный номер, изменив текущее решение и добавив 10 * текущий номер.

Этот вид инварианта очень полезен при тестировании вашего алгоритма - некоторые кодеры будут регулярно включать assert заявление для проверки этих типов инвариантов.

Может быть несколько инвариантов - в вашем случае существует ряд неравенств, которые остаются верными.