Технология программирования. - 47 стр.

UptoLike

Рубрика:

- 49 -

ных. Завершимость – свойство, которое интересно нам в связи с возможностью

избежать ошибок программ. Из рассмотренных трёх базовых структур программ

источником зацикливания может быть только конструкция повторения. Поэтому

для доказательства завершимости программы достаточно уметь доказывать завер-

шимость оператора цикла. Для этого полезна

теорема 7 [1]:

Пусть F – целочисленная функция, которая зависит от состояния ИС

и удовле-

творяет двум условиям:

1) если для данного состояния ИС предикат Q истинен, то F > 0;

2) функция F убывает при изменении состояния ИС в результате выполнения

оператора S.

Тогда выполнение оператора цикла

ПОКА Q ДЕЛАТЬ S ВСЁ ПОКА

завершается и программа не зацикливается.

Доказательство:

Пусть IS – некоторое состояние ИС перед выполнением оператора цикла, и

пусть F(IS) = k. Если предикат Q(IS)

ложен, то выполнение оператора цикла за-

вершается. Если же предикат Q(IS) истинен, то по условию теоремы к > 0, т.е. опе-

ратор S выполняется один или более раз. После каждого выполнения оператора S

по условию теоремы значение функции F уменьшается, а так как перед выполне-

нием оператора S предикат Q должен быть истинен (по семантике оператора цик-

ла

), то значение функции F в этот момент должно быть больше 0 (по условию тео-

ремы).

Поэтому в силу целочисленности функции F оператор S в этом цикле не может

быть выполнен более k раз. Теорема доказана.

10. Тестирование и отладка – важнейшие этапы разработки ПС

Отладка ПС – это деятельность, в результате которой обнаруживаются и ис-

правляются ошибки ПС в процессе выполнения его программ.