Учебное пособие по методам Флойда, страница 5

Точки сечения. Выберем множество точек сечения блоксхемы таким образом, чтобы каждый цикл в блок-схеме содержал,по крайней мере, одну точку сечения, и некоторое фундированное34множество (W, ≺ ). Для каждой точки сечения i выберем индуктивное утверждение qi(x, y). Построим условия верификации для индуктивных утверждений qi(x, y) согласно методу, рассмотренномуранее, для начальных базовых и промежуточных базовых путей идокажем их истинность.Шаг 2.

Оценочные функции.Определим для каждой точки се-чения i оценочную функцию ui(x, y) : Dx  Dy  Wi, где Wi ⊇ W, исформулируем условие корректности определения оценочной функции: x  Dx  y  Dy [ (x) ∧ qi(x, y)  ui(x,y)  W]Это условие утверждает, что для всех векторов значений переменных x и y, удовлетворяющих в точке сечения i индуктивномуутверждению qi(x, y), оценочная функция ставит в соответствиеэлемент множества W (а не его надмножества).Шаг 3.

Условия завершимости.Сконструируем для каждогопромежуточного базового пути , начинающегося в точке сечения iи завершающегося в точке сечения j, условие завершимости: x  Dx  y  Dy [ (x) ∧ qi(x, y) ∧ R(x, y)  ( ui(x,y) ≻uj(x, r(x, y) ) ) ]Условие завершимости утверждает, что если предикат q i(x, y)истинен для некоторых значений переменных x и y, и эти значениятакие, что, начиная из точки сечения i, вычисление пойдет по пути, то результат оценочной функции u j(x, y) на значениях переменных x и y после прохождения по пути  будет меньше результатаоценочной функции ui(x, y) на исходных значениях.35Шаг 4. Условия успешности вычисления функций.

Для доказательства полной корректности необходимо показать, что функции,приписанные операторам блок-схемы, которые могут равняться ,не вызываются с такими аргументами, при которых они равны .Для оператора START, которому приписана функция f, составим следующее условие успешности вычисления функции f: x  Dx [ (x)  f(x) ≠ ω ]Для каждого пути , начинающегося в точке сечения i, не содержащего в себе других точек сечения и завершающегося передоператором ASSIGN с функцией g, составим следующее условиеуспешности вычисления функции g: x  Dx  y  Dy [(x) ∧ qi(x, y) ∧ R(x, y)  g(x, r(x, y))≠ ω]Аналогичные условия составим для каждого пути , начинающегося в точке сечения i, не содержащего в себе других точек сечения и завершающегося перед оператором HALT с функцией h: x  Dx  y  Dy [(x) ∧ qi(x, y) ∧ R(x, y)  h(x, r(x, y))≠ ω]Теорема 2. (Метод фундированных множеств Флойда)Пусть даны блок-схема P и ее входной предикат .

Выполнимследующие действия:1. Выберем точки сечения с подходящим набором индуктивных утверждений и фундированное множество;2. Выберем подходящий набор оценочных функций;3. Построим условия верификации для всех базовых начальных и промежуточных путей, условия корректности опре36деления всех оценочных функций и условия завершимостидля всех промежуточных базовых путей.4. Построим условия успешности вычисления функций, приписанных всем операторам START, ASSIGN и HALT.Если все условия на шагах 3 и 4 истинны, то блок-схема Pуспешно завершается на .Доказательство теоремы предоставляется читателю в качествеупражнения.Замечания к методам ФлойдаПри доказательстве полной корректности блок-схемы на этапедоказательства завершаемости можно использовать те же точки сечения и индуктивные утверждения, которые были использованыдля доказательства частичной корректности.

Это позволит сократить объем доказательства полной корректности. Однако если индуктивные утверждения достаточно громоздки, при доказательствезавершаемости следует рассмотреть возможность использования«новых» индуктивных утверждений, более компактных.После успешного доказательства частичной корректности с некоторыми индуктивными утверждениями можно использовать ихследствия при доказательстве успешной завершимости и не составлять и передоказывать условия верификации для них.Далеко не всегда удается сразу предложить набор индуктивныхутверждений, достаточный для доказательства частичной корректности или завершаемости. При этом если в процессе доказательства обнаружится, что выбранного индуктивного утверждениянедостаточно, необходимо начать доказательство частичной кор37ректности сначала, чтобы составить все необходимые условияверификации с нужными измененными индуктивными утверждениями и доказать их истинность.

К сожалению, этим часто пренебрегают, что ведет к неверным доказательствам полной корректности, например, из-за того, что измененные индуктивные утверждения не являются корректными для путей, уже ранее рассмотренных в этом доказательстве.Тем не менее, в некоторых случаях можно вносить такое «изменение» в индуктивное утверждение как «приписывание предусловия». А именно, в условиях верификации, завершимости и корректности определения оценочной функции можно дописывать вконъюнкцию посылки импликации входной предикат, т. к.

значения входных переменных не меняются во время выполнения блоксхемы. Например, условие верификации для промежуточного базового пути можно изменить следующим образом: x  Dx  y  Dy [ pi(x, y) ∧ (x) ∧ R(x, y)  pj( x, r(x,y) ) ]Доказательство полной корректности программы целочисленного деления при помощи методов ФлойдаДокажем полную корректности блок-схемы целочисленного деления, представленной на рисунке 2, относительно следующей спецификации:  (x1  0) ∧ (x2 > 0)  (x1 = z1x2 + z2) ∧ (0  z2 < x2)Доказательство разбиваем на два этапа: сначала покажем частичную корректность этой блок-схемы относительно указанной38спецификации (при помощи метода индуктивных утверждений), азатем–завершаемостьблок-схемы(припомощиметодафундированных множеств).Доказываем частичнуюкорректность.Выберемвкачествеединственную точку сечения – В.

Она разбивает единственныйцикл в этой блок-схеме. Сопоставим этой точке сечения индуктивное утверждение p(x1, x2, y1, y2)  (x1 = y1x2 + y2) ∧ (y2  0) – см.рисунок 3.Необходимоследующихпутейвсоставитьусловияблок-схеме:верификацииSTART – B,дляB – T – B,B – F – HALT.Условие верификации для пути START – B: x1, x2  Z [ (x1, x2)  p(x1, x2, 0, x1) ]Подставляем определения предикатов: x1, x2  Z [ (x1  0) ∧ (x2 > 0)  (x1 = 0 · x2 + x1) ∧ (x1  0) ]Очевидно, что данное утверждение истинно.Условие верификации для пути B – T – B: x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ p(x1, x2, y1, y2) ∧ (y2 x2)  p(x1, x2, y1 + 1, y2 - x2) ]Подставляем определения предикатов: x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ (x1 = y1x2 + y2) ∧ (y2 0) ∧ (y2  x2)  (x1 = (y1 + 1)·x2 + y2 - x2) ∧ (y2 - x2  0) ]Достаточно раскрыть скобки и убедиться в истинности этогоутверждения.Условие верификации для пути B – F – HALT:39 x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ p(x1, x2, y1, y2) ∧  (y2 x2)  (x1, x2, y1, y2) ]Подставляем определения предикатов: x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ (x1 = y1x2 + y2) ∧ (y2 0) ∧ (y2  x2)  (x1 = y1x2 + y2) ∧ (0  y2 < x2) ]Очевидно, что и это утверждение истинно.Тем самым, согласно теореме 1 блок-схема целочисленного деления на рисунке 2 является частично корректной относительноуказанной выше спецификации.Доказываем завершаемость блок-схемы целочисленного деленияна рисунке 2 при всех значениях входных данных, удовлетворяющих предикату   (x1  0) ∧ (x2 > 0).В качестве множества точек сечения выберем единственнуюточкусеченияВдоказательства(туже,частичнойкотораябылаиспользованакорректности)идлястандартноефундированное множество ({0, 1, 2, …}, <).

В этой точке сечениявыберемтожеиндуктивноеутверждение,котороебылоиспользовано при доказательстве частичной корректности, а вкачестве оценочной функции выберем функцию u  y2 (см.рисунок 4).Вэтомслучаеусловияверификацииповторносоставлять не нужно – их мы возьмем из доказательства частичнойкорректности.Необходимосоставитьусловиекорректностиопределения оценочной функции для точки сечения В и условиезавершимости для единственного промежуточного базового путиB – T – B.40START:( y1, y2 )  ( 0, x1 )p(x1, x2, y1, y2)  (x1 = y1x2 + y2)BTDy2  x2( y1, y2 )  ( y1+1, y2- x2 )F∧(y2  0)u(x1, x2, y1, y2)  y2HALT:( z1, z2 )  ( y1, y2 )Рисунок 4.

Доказательство завершаемости программы целочисленного деленияУсловие корректности определения оценочной функции в точкесечения В: x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ p(x1, x2, y1, y2)  u(x1,x2, y1, y2)  W]Подставляем определения предиката p, функции u и множестваW: x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ (x1 = y1x2 + y2) ∧ (y2 0)  (y2  0) ]Очевидно, что это условие истинно.Условие завершимости для пути B – T – B: x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ p(x1, x2, y1, y2) ∧ (y2 x2)  u(x1, x2, y1, y2) > u(x1, x2, y1 + 1, y2 - x2) ]Подставляем определения предиката p и функции u:41 x1, x2, y1, y2  Z [ (x1  0) ∧ (x2 > 0) ∧ (x1 = y1x2 + y2) ∧ (y2 0) ∧ (y2  x2)  y2 > y2 - x2 ]Это условие является истинным.Тем самым, согласно теореме 2 блок-схема целочисленногоделения на рисунке 2 завершается при всех значениях входныхданных, удовлетворяющих предикату .Нами доказана частичная корректность и завершаемость блоксхемы, а, значит, доказана полная корректность.Задачи и упражненияВ некоторых задачах верифицируемая программа записана ввиде функции на языке программирования Си.