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

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

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

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

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

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

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

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

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

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

В качестве примера рассмотрим программу C₀ целочисленного деления натуральных чисел 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) для нашей программы, имеющего вид:

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

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

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

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

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

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

E₀=b+2∙y>0 & y>0 ® E₀>b+y,

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

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

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

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

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

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

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

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

р → (E>0) (1’)

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

{E₀=E>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 =E₀} {0< y – t =E₀} – А1,

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

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

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

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

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

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

(y – t) +1) =E₀ → (y – t) < E₀,

откуда вытекает справедливость условия (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, имеем:

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

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

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

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

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

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

E₀ = (y- t)+1 ® E₀ > 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 является инвариантом цикла, а следовательно, цикл не завершается.

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