Программа как математический объект: Методические указания для самостоятельного изучения темы и выполнения РГР, страница 22

                         if  y ³ 0 then  y:= x - y else x := y- x;

                         if  x ³ 0 then  x:= x - y else y := y - x;

Данная программа в виде условных правил  имеет следующий вид:

(  x ³ 0 ® x:= x + y | истинно®y := y + x)

 (  y ³ 0 ® y:= x - y | истинно®x := y- x)

 (  x ³ 0 ® x:= x - y | истинно®y := y - x)

 Преобразуем эту программу в последовательность разделяющихся правил:

(  x ³ 0 ® x:= x + y | x < 0 ®y := y + x)

 (  y ³ 0 ® y:= x - y | y < 0®x := y- x)

(  x ³ 0 ® x:= x - y |   x < 0®y := y - x)

Рассмотрим  трассировочные таблицы только для двух путей (всего их восемь), остальные строятся аналогично.

Вариант 1.1.1

Фрагмент

 Условие

            x

           y

 x := x + y

 x0 ³ 0

  x1 =  x0 + y0

 y1 = y0

 y := x - y

 y1  ³ 0

 x2 = x1

 y2 = x1 - y1

 x := x - y

 x2  ³ 0

 x3 = x2 - y2

 y3 = y2

Выводы условия: x0 ³ 0 L y1  ³ 0 L x2  ³ 0 = x0 ³ 0 L y0  ³ 0 L x1  ³ 0 =

 x0 ³ 0 L y0  ³ 0 L x0 + y0 ³ 0  = x0 ³ 0 L y0  ³ 0

Выводы присваивания: x3 = x2 - y2 = x1 - (x1 -  y1) = y1 = y0

                                        y3 = x1 -  y1 = (x0 + y0 ) - y0 = x0

функция первой ветки: x0 ³ 0 L y0  ³ 0 ® x, y := y, x

Вариант 1.1.2

Фрагмент

 Условие

            x

           y

x := x + y

 x0 ³ 0

  x1 =  x0 + y0

 y1 = y0

 y := x - y

 y1  ³ 0

 x2 = x1

 y2 = x1 - y1

 y := y - x

 x2  < 0

 x3 = x2

 y3 = y2 -x2

Выводы условия: x0 ³ 0 L y1  ³ 0 L x2  < 0 = x0 ³ 0 L y0  ³ 0 L x1  < 0 =

 x0 ³ 0 L y0  ³ 0 L x0 + y0 < 0  = ложно

присваивание  не имеет смысла.

Объединяя  все варианты, получим функцию, которая определяется разделяющимся правилом, состоящим из шести частей:

( x ³ 0 L y ³ 0 ® x, y := y, x |

x = 0 L y <0 ® x, y := -y - x, y |

x > 0 L y < 0 ® x, y :=  - x, y+ x |

x < 0 L x + y ³ 0 ® x, y := x, - y - x |

x < 0 L x + y < 0  L y ³ 0® x, y := - x, y+ x |

x < 0 L y < 0 ® x, y := y, x )

Этому правилу соответствует диаграмма в плоскости x, y, показанная на рис.35. Данное разделяющееся правило преобразуем в следующее условное правило:

( x ³ 0 L y ³ 0 ® x, y := y, x |     

x = 0 ® x, y := -y - x, y |

x > 0 ® x, y :=  - x, y+ x |

 y < 0 ® x, y := y, x |

        x + y < 0 ® x, y := - x,  y+ x |

истинно ® x, y := x, - y - x )

4.4.6  Верификация программ типа for _ do.

 Программу типа  for _ doможно рассматривать как сокращённую форму записи обобщённой последовательной  программы. Например, программа типа

Q = fori : Î 1 to6 by 2dos := max ( i, s + i ) od является сокращённой записью обобщённой последовательности

R = s := max ( 1, s + 1); s := max ( 3, s + 3); s := max ( 5, s + 5);

В этом случае программная функция программ Q и R легко определяется по трассировочной таблице:

Фрагмент

                 s

s := max (1, s +1)

s1 := max (1, s0 +1)

s := max (3, s +3)

s2 := max (3, s1 +3)

s := max (5, s +5)

s3 := max (5, s2 +5)

с выводом  s3 = s := max (5, s 2+5) = max (5,  max (3, s1 +3) +5) =

 max (8, s1 +8)  = s := max (8,  max (1, s0 +1) +8) = s := max (9, s0 +9) и функцией программы    s := s := max (9, s +9).

Однако, если программа типа for _ do дана в общём  виде с параметром n, определяющим размерность цикла, например:

Pn = fori : Î 1 ton by 2dos := max ( i, s + i ) od, то в этом случае для доказательства правильности программы используется метод математической индукции. При использовании метода математической индукции возможны две стратегии в определении программной функции for _ do, основанные на выборе переменной, по которой проводится индукция. В качестве такой переменной можно выбрать целочисленную переменную из описания списка for _ do. При другом варианте ею может быть размер самого списка for _ do. В любом случае используется классическая схема математической индукции: