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

H(k) = ([P_k] = h(k)) , где h(k) является предполагаемой функцией P_k программы for _ do. Теперь,  чтобы выполнить индукцию, мы должны доказать,что

1) H(1) истинно,

2) (k ³1 L H(k)) ® H(k + 1).

3) из чего выводится импликация k³1  ® H(k ).

Например, рассмотрим верификацию программы fori : Î 1 to100 by 2dos := max ( i, s + i ) od  1) для индукции по переменной с предельным  значением 100;

2) для индукции по размеру списка с предельным значением 50. Выбор стратегии зависит от задачи. Если параметр  n используется в do - части программы P, то уместно выбрать первую стратегию, в противном случае выбираем вторую. В рассматриваемой задаче do - часть не  зависит от n, проведём индукцию по размеру списка, обозначив его, size(n).   Нетрудно заметить, что

size(n) = (n + odd(n))/2. Далее, обозначив size(n) через к, выведем функцию программы для k= 1, 2, 3 .

k	Функция  программы
1	s := max ( 1, s + 1)
2	s := max ( 4, s + 4)
3	s := max ( 9, s + 9)

Выдвигаем следующую гипотезу:

H(k) = ([P_k] = (s := max(k **2, s + k**2))), k = size(n). При k = 1 гипотеза верна, предположим, что она верна при k = t, H(k) = ([P_k] = (s := max(t **2, s + t**2))), докажем, что она верна при k= t+1. Так как,  тело цикла  fori : Î 1 ton by 2dos := max ( i, s + i ) od выполняться  t + 1 раз, то  последовательность операторов тела цикла max ( 1, s + 1 ); max ( 3, s + 3); . . . max ( i, s + i ) можно разбить на две части: первая равна размеру списка t  и согласно гипотезе может быть заменена на оператор  s := max(  t**2, s + t**2) , вторая - один оператор тела цикла  и его можно записать как s := max( 2*t +1, s + 2*t+1). Последняя формула выводится следующим  образом: выражаем i через t из формулы size(n) = (n + odd(n))/2.  t+ 1 = i + odd(i))/2  ® i = (t + 1)*2 - odd(i) = 2*t +2 - 1 = 2*t + 1 ( odd(i) = 1, так как для того, чтобы тело цикла выполнилось ещё раз i должен быть нечётным ). Таким образом,  исходную программу мы свернули к последовательности R = s := max(t**2,s +  t**2)

                  s := max( 2*t +1, s + 2*t +1), теперь докажем, что

 [R]=s := max( (t+2)**2, s+(t+1)**2)

Равенства трассировочной таблицы для программы R имеют вид

                 s₁ = max(t**2,s₀ + t**2)

                 s₂  = max(2*t+1, s₁+2*t+1)

вывод функции s₂ = max(2*t  +1, t**2+2*t+1, s₀+t**2+2*t+1)

                               = max((t+1)**2,s₀+(t+1)**2).

Функция [R] = max((t+1)**2,s+(t+1)**2) и она равна H(t+1),поэтому

k ³ 1 ® H(k) =([P]=(s:= max(k**2, s+k**2))), что  и требовалось доказать.

    4.5  Инварианты цикла при доказательстве правильности программ

4.5.1. Инварианты цикла

Инвариантом цикла программы с одним предикатом является логическое условие( предикат), которое неизменно удовлетворяется, когда вычисляется этот предикат.            

 Например, в программе сложения(u, v ³0 ® u, v:= u + v, 0)

while v¹0 do u,v := u +1, v -1 od

предикат u + v = u₀ + v₀ принимает значение истинно при входе в цикл и при каждой итерации цикла. Поэтому этот предикат является инвариантом. Этот факт отображается логическим комментарием, так называемым, комментарием инвариантного отношения, который приписывается ключевому слову while:

 while [u + v = u₀ + v₀]

v¹0

 do u,v := u +1, v -1

 od

 Инварианты, если они известны, можно использовать как альтернативу методам верификации, описанным в теореме правильности. Инвариантное отношение записывается после ключевого слова while перед while - тестом. Оно всегда принимает значение  не зависимо от того, какое значение - истинно или ложно принимает while _ тест. Чтобы доказать, что предикат является инвариантом для некоторой программы типа while _ do, достаточно доказать, используя метод индукции, что

1) предикат имеет значение истинно при входе в цикл while _do;