Помощничек
Главная | Обратная связь


Археология
Архитектура
Астрономия
Аудит
Биология
Ботаника
Бухгалтерский учёт
Войное дело
Генетика
География
Геология
Дизайн
Искусство
История
Кино
Кулинария
Культура
Литература
Математика
Медицина
Металлургия
Мифология
Музыка
Психология
Религия
Спорт
Строительство
Техника
Транспорт
Туризм
Усадьба
Физика
Фотография
Химия
Экология
Электричество
Электроника
Энергетика

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

Доказательство завершимости (незавершимости) программ

 

Кораблин Ю.П.

 

Очевидно, что операторами языка L, которые могут привести к незавершимости программы, являются команды цикла while B do C od repeat C until В. Для анализа завершимости циклов можно использовать инварианты цикла.

Условия завершимости цикла while B do C od

Пусть E - некоторое целочисленное выражение. Предположим, что справедливо утверждение:

Р & B ® (Е>O) (1)

и для любого выражения е0, принимающего целочисленные значения, справедливо:

{0<E=E0} C {0≤E<E0} (2)

Это означает, что утверждение Е ≥ 0 также, как и Р является инвариантом цикла, т.е. выражение E остается неотрицательным в течение итерационного процесса. Кроме того, условие (2) означает, что каждое выполнение программы C уменьшает значение выражения E. Таким образом, из справедливости (1) и (2), а также {Р & В} C {P} непосредственно следует вывод о конечности итерационного процесса, так как целочисленное выражение Е не может уменьшаться бесконечное число раз и оставаться положительным, как требует условие (1).

В качестве примера рассмотрим программу C0 целочисленного деления натуральных чисел x и y:

{х≥0 & y>0} а:=0; b:=x; while b≥y do {b+y>0} b:=b-y; а:=а+1 od {b+y>0}

Искомым выражением Е здесь является b+y, а инвариантом цикла утверждение b+y≥0.

Докажем вначале справедливость утверждения (1) для данной программы. Возьмем для этой цели в качестве Р утверждение y>0, являющееся инвариантом цикла. Доказательство того, что y>0 является инвариантом, тривиально, т.к. y>0 перед выполнением программы и нигде в программе не изменяется. При стандартной интерпретации на области целых чисел получаем, что утверждение y>0 & b>y ® b+y>0 справедливо.

Докажем теперь справедливость утверждения (2) для нашей программы, имеющего вид:

{E0=b+y>0} b:=b-y; a:=a+1 {E0>b+y≥0}.

Поскольку справедливо утверждение:

E0=b+y>0 & y>0 & b≥y ® E0=(b-y)+2∙y>0 & y>0 & (b-y)+y≥y,

то, по аксиоме А1 и правилу вывода R5, получаем:

{E0-b+y>0 & y>0 & b≥y} b:=b-y {E0=b+2∙y>0 & y>0 & b+y≥y}

Поскольку справедливы также утверждения:

E0=b+2∙y>0 & y>0 ® E0>b+y,

b+y≥y & y>0 ® b+y≥0,

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

{E0-b*y>0 & y>0 & b≥y} b:=b-y {E0>b+y≥0}.

Далее, по аксиоме А1, имеем:

{E0>b+y≥0} а:=а+1 {E0>b+y≥0}.

Применяя теперь правило вывода R2, получаем искомый результат. Таким образом, мы доказали и утверждение (2) для циклического участка нашей программы. Отсюда следует завершимость итерационного цикла, а следовательно, и всей программы.

Условия завершимости цикла repeat-until

Условия завершимости цикла repeat-until формулируются аналогично условиям для цикла while B do C od.

р → (E>0) (1’)

и для любого целочисленного выражения E0 справедливо

{E0=E>0} С {Е0>Е≥0} (2’)

где E - некоторое целочисленное выражение.

Это означает, что утверждение E≥0 является инвариантом цикла repeat-until, т.е. выражение Е остается неотрицательным в течение циклического процесса. Кроме того, условие (2') означает, что каждое выполнение команды (программы) С уменьшает значение выражения Е. Таким образом, из справедливости (1')и (2'), а также утверждений {P} C {Q}, Q & B → Р, следует вывод о конечности циклического процесса, так как целочисленное выражение Е не может уменьшаться бесконечное число раз и оставаться положительным, что требует условие (1').

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

Доказать завершимость следующих циклов для заданных исходных условий.

1. { (t < y) }while t ≠ у do s:=s+1; t:=t+1 od.

2. { (t < y) }repeat s := s + 1; t := t + 1 until t = у.

Решение:

Рассмотрим пример 1. Возьмем в качестве инварианта цикла утверждение P º t ≤ y. Очевидно, что это утверждение справедливо перед выполнением цикла, т.к. (s = о + t) & (t < y) → t ≤ y – справедливо.

Покажем, что P является инвариантом цикла.

(1) (t ≤ y) & (t ≠ у) → t < y – справедливо,

(2) t < y → t+ 1 ≤ y – справедливо,

а следовательно

(3) (t ≤ y) & (t ≠ у) → t+ 1 ≤ y – справедливо.

Далее имеем:

(4) {t+ 1 ≤ y } s := s + 1{t+ 1 ≤ y } – А1,

(5) {t+ 1 ≤ y } t:=t+1 {t ≤ y } – А1,

(6) {(t ≤ y) & (t ≠ у)} s:=s+1; t:=t+1 {t ≤ y } – R2(4,5),

(7) {t ≤ y } while t ≠ у do s:=s+1; t:=t+1 od {t ≤ y& (t = у) } – R4(6).

Отсюда вытекает, что P º t ≤ y является инвариантом цикла.

В качестве целочисленного выражения возьмем E º y – t.

Покажем, что для него выполняются условия (1) и (2) завершимости цикла.

(1) P&B → E> 0, т.е. t ≤ y& t ≠ у → y > t, а следовательно, y – t > 0, ч.т.д.

Далее покажем выполнение условия (2):

{0< y – t =E0} {0< y – t =E0} – А1,

{0< y – t =E0} s:=s+1 {0< y – t =E0} – А1,

0< y – t =E0 → 0< y – (t+1-1) =E0 – справедливо,

{0< y – (t+1-1) =E0} t:=t+1 {0< (y – (t –1)) =E0} – А1,

0< (y – (t –1)) =E0 → 0< (y – t) +1 =E0 – справедливо,

а следовательно справедливы следующие утверждения:

0< (y – t) +1 → 0 ≤ (y – t),

(y – t) +1) =E0 → (y – t) < E0,

откуда вытекает справедливость условия (2).

Из доказанных условий (1) и (2) вытекает завершимость цикла примера 1.

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

Доказать завершимость следующей программы:

{ true }x:= x0; у := у0; s := 0;

while x ≠ 0 do t := 0; while t≠y do {s=(x0- x) *y0+ t}s := s + 1; t := t + 1od;

x := x – 1 od

где x, у, х0, у0, s и t - неотрицательные целочисленные переменные.

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

Докажем вначале завершимость внутреннего цикла. В качестве инварианта внутреннего цикла возьмем P º y³t, а целочисленного выражения E = y- t. Нетрудно показать, что операторы, предшествующие внутреннему циклу, устанавливают инвариант P, т.к. из того, что y ³ 0 и t = 0 следует, что y³t. Далее, из этого условия, а также условия входа в цикл (t≠y), непосредственно следует, что y> t, а следовательно и y> t+1-1.

По аксиоме A1 имеем:

{ y> t+1-1} s := s + 1{ y> t+1-1},

{ y> t+1-1} t := t + 1 { y> t-1}.

Из последнего вытекает, что y³t. Отсюда, применяя правила вывода R2 и R5, получаем:

{y³t Ù t≠y } s := s + 1; t := t + 1{y³t }.

Отсюда, по правилу вывода R4, получаем, что P º y³t является инвариантом внутреннего цикла.

Покажем теперь справедливость условий (1) и (2) завершимости цикла.

Так как утверждение y³t Ù t≠y ® y> t справедливо, получаем, что E = y- t > 0. Таким образом, условие (1) выполнено. Далее, применяя аксиому A1, имеем:

{E0 = y- t > 0} s := s + 1{E0 = y- t > 0},

{E0 = y- (t +1-1) > 0} t := t + 1{E0 = y- (t-1) > 0}.

Поскольку справедливы утверждения:

E0 = y- t > 0 ® E0 = y- (t +1-1) > 0,

E0 = y- (t-1) > 0 ® E0 = (y- t)+1 > 0, то , применяя правила вывода R2 и R5, получаем:

{E0 = y- t > 0} s := s + 1; t := t + 1 {E0 = (y- t)+1 > 0}. Далее имеем:

E0 = (y- t)+1 ® E0 > E,

(y- t)+1 > 0 ® E ³ 0.

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

Для доказательства завершимости внешнего цикла можно взять в качестве инварианта этого цикла предикат P º x ³ 0, а в качестве целочисленного выражения E= x. Нетрудно показать, что P является инвариантом внешнего цикла. Доказательство справедливости условий (1) и (2) осуществляется по аналогии с приведенным выше доказательством условий завершимости внутреннего цикла.

Заметим, что неудача при попытке получить подходящее целочисленное выражение для доказательства завершимости не дает оснований для вывода о незавершимости программы для некоторых начальных значений переменных. Незавершимость программы в этом случае также требует доказательства.

Если мы подозреваем, что такой цикл не завершается, то требуется доказать, что не только Р, но и Р & В является инвариантом цикла, т.е. необходимо показать, что если Р & В истинно перед выполнением C, то оно будет истинно и после выполнения С. Отсюда следует незавершимость цикла.

Доказательство незавершимости позволяет также выяснить причины незавершения программы. Анализ этих причин позволяет вносить исправления в программу.

Проиллюстрируем сказанное на примере рассмотренной выше программы целочисленного деления. Вместо начальных условий х≥0 & y>0 возьмем х≥0 & у≥0. В этом случае нетрудно показать, что для y=0 утверждение b≥y будет инвариантом цикла

while b≥y do b:=b-y; a:=a+1 od.

Докажем это, как обычно, в два этапа:

1) установка инварианта b≥y командами, предшествующими циклу;

2) сохранение этого инварианта командами тела цикла.

1) Легко показать, что:

{x≥0 & y=0} а:=0; b:=x {b=x & x≥0 & y=0}.

Далее, поскольку справедливы утверждения:

b=x & x≥0 → b≥0,

b≥0 & y=0 → b≥y & y=0,

получаем по правилу вывода R5:

{х≥0 & y=0} а:=0; b:=х {b≥y & y=0},

т.е. b≥y истинно перед выполнением цикла.

2) Применяя аксиому А1, получаем:

{(b-y)+y≥y & y=0} b:=b-y {b+y≥y & y=0}.

Поскольку справедливо утверждение:

b+y≥y & y=0 → b≥y,

то, по правилу вывода R5, получаем:

{b≥y & y=0} b:=b-y {b≥y}.

Далее, применяя аксиому A1, имеем:

{b≥y} a:=a+1 {b≥y}.

Далее, по правилу R2, получаем:

{b≥y & y=0} b:=b-y; a:=a+1 {b≥y},

откуда следует, что b≥y является инвариантом цикла, а следовательно, цикл не завершается.

 




Поиск по сайту:

©2015-2020 studopedya.ru Все права принадлежат авторам размещенных материалов.