Иванов А.С. Информатика

Подождите немного. Документ загружается.

Теперь посмотрим, каким соотношениям должны удовлетворять перемен-

ные на разных участках кода.

{((x ≥ 0) ∧ (y > 0))}

q = 0;

r = x;

{((x = q ∗ y + r) ∧ (0 ≤ r))}

while (r ≥ y) {

{((x = q ∗ y + r) ∧ (0 < y ≤ r))}

r = r − y;

q = 1 + q; }

{((x = q ∗ y + r) ∧ (0 ≤ r < y))}

Критерий корректности программы выражается соотношением

(x = q ∗ y + r) ∧ (0 ≤ r < y),

которое должно иметь место при завершении программы, если соотношение

(х ≥ 0) ∧ (у > 0) справедливо перед ее выполнением. Именно это и следует

доказать.

Рассмотрим сначала цикл в приведенной программе, представленный

на рис. 7.11. В этом примере B имеет вид (r ≥ у). Если теперь заме-

тить, что выходное соотношение на рис. 7.11 может быть переписано как

(x = q ∗ у + r) ∧ (r ≥ 0) ∧ ¬(r ≥ у), то ясно, что это как раз и есть P ∧ ¬B,

где

P − это (x = q ∗ y + r) ∧ (r ≥ 0). (7.22)

r≥ y

Ложь

Истина

{((x = q ∗ y + r) ∧ (0 ≤ r))}

{((x = q ∗ y + r) ∧ (0 ≤ r < y))}

Рис. 7.11

Другими словами, наша задача при верификации рис. 7.11 показать, что

{P }while(r ≥ y)S

{P ∧ ¬(r ≥ y)}, где инвариант цикла P задается соотно-

шением (7.22). Но правило вывода (7.18) гарантирует, что это утверждение

должно быть истинным постольку, поскольку можно доказать

{P ∧ (r ≥ y)}S

{P } (7.23)

для P , задаваемого (7.22) и S

, задаваемого {r = r − у; q = 1 + q; }.

Теперь заметим, что

(x = q ∗ y + r) ∧ (r ≥ 0) ∧ (r ≥ y) → (x = (1 + q) ∗ y + (r − y)) ∧ (r − y ≥ 0).

Вспоминая правило вывода для оператора присваивания, получим:

{(x = (1 + q) ∗ y + r−y) ∧ (r−y≥ 0)}r = r−y; {(x = (1 + q) ∗ y + r) ∧ (r≥ 0)}

{(x = (1 + q) ∗ y + r) ∧ (r ≥ 0)}q = 1 + q; {(x = q ∗ y + r) ∧ (r ≥ 0)}.

Из правила вывода для составного оператора и правила консеквенции

следует:

{P ∧ (r ≥ y)}{r = r − y; q = 1 + q; }{P }, (7.24)

которое есть в точности выражение (7.23), необходимое для доказательства.

Таким образом, получаем

{P }while(r ≥ y)S

; {P ∧ ¬(r ≥ y)}. (7.25)

Следующий шаг состоит в проверке выполнения условия

{(x ≥ 0) ∧ (y > 0)}{q = 0; r = x; }{(x = q ∗ y + r) ∧ (r ≥ 0)}. (7.26)

Действительно,

(x ≥ 0) ∧ (y > 0) → ( x = 0 ∗ y + x) ∧ (x ≥ 0);

{(x = 0 ∗ y + x) ∧ (x ≥ 0)}q = 0; {(x = q ∗ y + x) ∧ (x ≥ 0)};

{(x = q ∗ y + x) ∧ (x ≥ 0)}r = x; {(x = q ∗ y + r) ∧ (r ≥ 0)}.

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

ло вывода для составного оператора получаем (7.26).

Теперь из (7.25), (7.26) и правила вывода для составного оператора сле-

дует:

{(x ≥ 0) ∧ (y > 0)}

q = 0; r = х;

while(r ≥ у){r = r − у; q = 1 + q; }

{(x = q ∗ y + r) ∧ (0 ≤ r < y)}.

Условие y > 0 не использовалось при доказательстве частичной коррект-

ности, однако оно будет играть существенную роль при доказательстве того,

что алгоритм действительно завершается.

Список рекомендуемой литературы

Алагич С., Арбиб М. Проектирование корректных структурированных про-

грамм. М.: Радио и связь, 1984. 284 c.

Ахо А., Ульман Д., Хопкрофт Д. Структуры данных и алгоритмы. М.: Ви-

льямс, 2007. 400 c.

Брой М. Информатика: В 3 ч. Ч. 1. М.: Диалог-МИФИ, 1996. 300 c.

Брукшир Д. Введение в компьютерные науки. М.: Вильямс, 2001. 688 c.

Гук М. Аппаратные средства IBM PC. СПб.: Питер, 2006. 816 с.

Кнут Д. Искусство программирования. Т. 1. Основные алгоритмы. М.: Ви-

льямс, 2006. 720 c.

Олифер В.Г., Олифер Н.А. Компьютерные сети. Принципы, технологии,

протоколы: Учебник для вузов. СПб.: Питер, 2001. 672 c.

Фомин С.В. Системы счисления. M.: Наука, 1987. 48 с.

Учебное издание

Иванов Александр Сергеевич

ИНФОРМАТИКА

Учебное пособие

Оригинал-макет подготовлен А.С. Ивановым в пакете L

X 2

Подписано в печать 19.11.2009. Формат 60× 84 1/16. Бумага офсетная.

Гарнитура Times New Roman. Печать RISO. Объем 5,25 печ. л. Тираж 200 экз. Заказ 293.

ООО Издательский центр «Наука»

410600, г. Саратов, ул. Пугачевская, д. 117, оф. 50

Отпечатано с готового оригинал-макета

Центр полиграфических и копировальных услуг

Предприниматель Серман Ю.Б. Свидетельство № 3117

410600, г. Саратов, ул. Московская, д. 152, оф. 19, тел. 26-18-19, 51-16-28