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

Трассировочная таблица позволяет путём систематического исключения всех промежуточных значений индексов, начиная с  конечных значений, вывести функцию программы:

                                      x₃ = x₂ - y₂ = x₁  -  (x₁ - y₁) = y₁ =y₀

                                      y₃ = y₂  = x₁ - y₁ = x₀  -+ y₀ - y₀ = x₀

 Таким образом, функция программы этой  последовательности представляет собой присваивание вида x, y:= y, xпри котором переменные обмениваются значениями.

   Заметим, что более привычный для нас обмен реализуется последовательностью присваиваний:

1) initial t := x

2) x :=  y

3) y :=  t

4) free t

Эта последовательность имеет трассировочную таблицу:

Фрагмент	t	x	y
1. initial t := x	t1 = x0	x1 = x0	y1 = y0
2. x :=  y	t2 =  t1	x2 =  y1	y2 =  y1
3. y :=  t	t3 =  t2	x3 = x2	y3 =  t2
4. free t	free	x4 = x3	y4   = y3

вывод:x₄ = x₃ = x₂ = y₁ = y₀;   y₄ = y₃ = t₂ = t₁ = x₀

функцию программы: x, y:= y, x.

4.4.2    Разделяющиеся условные правила

Чтобы доказать, что программа типа if _then _ else (ifp then G else H fi) правильно выполняет функцию f, необходимо верифицировать отношения:

f = [if p then G else H fi] и f Ì [if p then G else H fi]

Процесс верификации может повлечь за собой сравнение условных правил, потому что функция программы if _then _ else может быть точно преобразована в форму условного правила.

 Например,

[if p then G else H fi] = ( p ® [G] | Øp  ® [H] )

В общем случае f, [G], [H] могут быть сами заданы условными правилами; поэтому необходимо уметь упрощать их с целью сравнения  и определения  программной функции. Для этого введём понятие разделённых предикатов: два предиката p_i и p_j разделены, если  p_i L p_j º ложь, а условное правило   в случае разделения всех предикатов называем разделяющимся правилом.

Разделяющееся правило может оказаться более удобным для верификации, чем условное правило. К тому же его легко вывести, логически умножая каждый предикат на отрицание каждого и предыдущих предикатов. Таким образом, условное правило (p₁ ® r₁ | p₂ ® r₂ | p₃ ® r₃ | . . .) совпадает по результату с разделяющимся правилом (p₁ ® r₁ | Øp₁ L p₂ ® r₂ | Øp₁ LØ p₂ Lp₃ ® r₃ | . . . ), а разделяющееся правило (q ₁ ® s₁ | q₂ ® s₂ | q₃ ® s₃ | . . .) даёт такой же результат, как  и условное правило (q₁ ® s₁ | q₁  V q₂  ® s₂ | q₁ V q₂ V q₃ ® s₃ | . . .)

Отметим, что в каждом предикате последнего условного правила можно опустить любой член, кроме последнего; таким образом, разделяющееся правило можно преобразовать в одно из многочисленных условных правил.

Разделяющееся правило обладает следующим свойством: произвольная перестановка принадлежащих ему правил не  изменяет результата самого правила. Это правило лежит в основе верификации условных правил и их преобразования  в более простые эквивалентные условные правила.

4.4.3  Преобразование условных правил

Алгоритм преобразования:

1) преобразовать данное условное правило в эквивалентное ему разделяющееся правило;

2) преобразовать любым удобным способом разделяющееся правило, переставляя принадлежащие ему правила;

3) выполнить обратное преобразование разделяющегося правила в некоторое простое эквивалентное условное правило.

Пример: 1) исходное условное правило:

(x>0 ® z  := max (x, y) | y >0  ® z  := min (x, y));

2) раскроем функции max и min через условные правила, получим вложенное условное правило:

 (x>0®( x > y®z  := x | истинно®z := y) | y>0®

( x < y  ® z  := x | истинно  ®z := y) );

3) преобразуем в разделяющиеся правила:

(x>0®( x > y®z  := x | x £ y  ®z := y) | x £0 L y>0®

( x < y  ® z  := x | x ³ y ®z := y) );

4) введём внешние предикаты во внутренние:

                      (x > 0 L x > y ® z := x |