Нахождение инвариантов для циклов While

[lis87]

Задача нахождения максимального делителя (кроме самого числа). Без операции деления.
Для внутреннего цикла инвариант, я так поняла, A=R-YQ. Для внешнего не пойму. Инварианты нужны для доказательства корректности. Заранее спасибо за любые советы и помощь!
//A - входное число
//Y-искомый делитель, R-остаток от деления X на Y, Q-второй делитель <=Y
Y=A-1; R=A;
While (Y>0) and (R<>0) do
Begin
Y=Y-1; R=A; Q=0;
While (Y<=R) do
Begin
R=R-Y; Q=Q+1;
end
End;

[arseniiv]

(Настоятельный совет по какому-то, хотя бы показанному ниже, оформлению)

В следующий раз оформляйте код вот так:

Используется синтаксис Pascal

// A — входное число
// Y — искомый делитель, R — остаток от деления X на Y, Q — второй делитель <= Y
Y := A - 1;
R := A;
while &#40;Y > 0&#41; and &#40;R <> 0&#41; do begin
  Y := Y - 1;
  R := A;
  Q := 0;
  while Y <= R do begin
    R := R - Y;
    Q := Q + 1;
  end; // чтобы не было ошибок, если придётся добавить операторы после этого, лучше ; ставить всегда
end;
 

(Если это Pascal/Delphi, присваивание ведь записываться должно :=, а иначе надо другой (Algol, что ли?) будет вписать.)

Теперь легче разбираться в коде. И инвариант внешнего цикла найти, думаю.

P. S. Странно, что-то со скобками.

[lis87]

Да, согласна, написано коряво. Французский с нижегородским. Но что имелось в виду вроде бы более менее прозрачно. Если нет, то допишу. Оперативный ответ, не ожидала)

[arseniiv]

(Оффтоп)

lis87 в сообщении #388759 писал(а):

Оперативный ответ

Зато почти не по существу…