Если при возврате управления из
function Find_Key(A: A_Type; Key: Integer)
return Integer is
I: Integer := 100; -- Поиск с конца
begin
A(0) := Key; -- Установить «часового»
while A(l) /= Key loop
I:=I-1;
end loop;
return I;
end Find_Key;
Если при возврате управления из функции значение I равно нулю, то Key в
массиве нет; в противном случае I содержит индекс найденного значения.
Этот код более эффективен, цикл чрезвычайно прост и может быть легко про-
верен.
6.6. Инварианты
Формальное определение семантики операторов цикла базируется на концепции инварианта: формулы, которая остается истинной после каждого выполнения тела цикла. Рассмотрим предельно упрощенную программу для вы- числения целочисленного деления а на b с тем, чтобы получить результат у:
у = 0;
|
C |
while (х >- b) { /* Пока b «входит» в х, */
х -= b; /* вычитание b означает, что */
у++; /* результат должен быть увеличен */
}
и рассмотрим формулу:
a = yb +х
где курсивом обозначено значение соответствующей программной переменной. После операторов инициализации она, конечно, будет правильной, поскольку у = 0 и х = а. Кроме того, в конце программы формула определяет, что у есть результат целочисленного деления а/b при условии, что остаток х меньше делителя b.
Не столь очевидно то, что формула остается правильной после каждого выполнения тела цикла. В такой тривиальной программе этот факт легко увидеть с помощью простой арифметики, изменив значения х и у в теле цикла:
(у + \)b + (х-b)=уb+b+х-b=уb+х=а
Таким образом, выполнение тела цикла переводит программу из состояния, которое удовлетворяет инварианту, в другое состояние, которое по-прежнему удовлетворяет инварианту.
