Информатика и выч. техника \ Информатика

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

            0 = 0

          a*x+y = a0*x0+y0

                   a = a0

Второй инвариант представляет интерес, т.к. характеризует функцию. Учитывая третье сотношение  a = a0, предикат a*x+y = a0*x0+y0 перепишем a0 *(x - x0) = y0 - y . 1) этот предикат верен перед выполнением цикла, т.к.  x = x0, а  y = y0; 2) этот предикат выполняется во время выполнения цикла a0 *(x0 -1 - x0) = y0 - y0 -a; 3) после выполнения цикла x = 0.  Следовательно,  получаем - a0*x0 = y0  - y, а это есть предикат y = a0*x0+y0 L x = 0, что соответствует функции программы.

Пример 2

  Необходимо определить  программную функцию программы P1.

 P1 = do a:= a – b; q := q + 1; until a < b od;

Предположим, что такой функцией является функция

f = (if a ≥ 0 → a,b,q := (a-b) mod b,b,q + (a-b) div b + 1).

       Для доказательства правильности программы (do g until p od) можно использовать положение теоремы правильности для данной элементарной программы, а можно преобразовать программу P2 в эквивалентную программ, в которой цикл (do g until p od) заменяется  циклом( while q do g od  b) и дальнейшее доказательство правильности опирается на теорему правильности для элементарной программы (while q do g od  ).

  Рассмотрим тот и другой случаи.

Случай первый

 Function (a, b, q – целые, положительные числа)

f = (if a ≥ 0 → a,b,q := (a-b) mod b,b,q + (a-b) div b + 1)

program

do a := a – b; q := q + 1; until a < b od

proof

term начальное значение  a ≥ 0 и b > 0 при каждой итерации а уменьшается на b, а b не изменяется, так что в итоге  until_тест примет значение истина.

until_test true  (p◦g → f) = (p◦g → g)

Фрагмент

условие

a

b

q

a := a – b;

a1= a0 – b0

b1=b0

q1 := q0

q := q + 1;

a2= a1

b2=b1

q2= q1+ 1

a < b

a2 < b2

a3= a2

b3=b2

q3 := q2

if a ≥ 0 → a,b,q := (a- b) mod b,b,q + (a-b) div b +1

a3 ≥ 0

а4= (a3-b3)mod b3

b4=b3

q4= q3+(a3- b3) div b3 + 1

Выводы: 

условие: a2 < b2 ^  a3 ≥ 0 → a1 < b1 ^  a2 ≥ 0 → a0  - b0 < b0 ^  a1 ≥ 0 → a0  - b0 < b0 ^   a0  - b0  ≥ 0 → a0   < 2b0 ^   a0   ≥ b0  → a0 = b0

присваивание: а4= (a3- b3) mod b3  =  (a2- b2)mod b2 = (a1- b1)mod b1 = (a0 – b0 –b0)mod b0 =  a0 mod b0   = a0  - b0 = 0 (из условия, что a0 = b0 )

q4= q3+(a3- b3) div b3 +1 =  q2+(a2- b2)div b2 +1 = q1+ 2+(a1- b1)div b1  = q0+ 2+( a0- b0 – b0 ) div b0 = q0+ 2+( b0- b0 – b0 ) div b0 = q0+ 2+(  – b0 ) div b0 = q0+ 2-1 = q0+ 1

pass

until_test false  (┐p◦g → f) = (┐p◦g →f◦ g)

Фрагмент

условие

a

b

q

a := a – b;

a1= a0 – b0

b1=b0

q1 := q0

q := q + 1;

a2= a1

b2=b1

q2= q1+ 1

a < b

a2 ≥ b2

a3= a2

b3=b2

q3 := q2

if a ≥ 0 → a,b,q := (a- b) mod b,b,q + (a-b) div b + 1

a3 ≥ 0

а4= (a3-b3)mod b3

b4=b3

q4= q3+(a3- b3) div b3 + 1

 Выводы: 

условие: a2 ≥ b2 ^  a3 ≥ 0 → a1  ≥ b1 ^  a2 ≥ 0 → a0  - b0  ≥ b0 ^  a1 ≥ 0 → a0  - b0  ≥  b0 ^   a0  - b0  ≥ 0 → a0    ≥ 2b0 ^   a0   ≥ b0  → a0  ≥ 2 b0

присваивание: а4= (a3- b3) mod b3  =  (a2- b2)mod b2 = (a1- b1)mod b1 = (a0 – b0 –b0)mod b0 = (a0 – b0 ) mod b0- b0 mod b0   = (a0  - b0 )mod b0

q4= q3+(a3- b3) div b3 +1 =  q2+(a2- b2)div b2 +1 = q1+ 2+(a1- b1)div b1  = q0+ 2+( a0- b0 – b0 ) div b0 = q0+ 2+( a0- b0) div b0– b0  div b0 = q0+ 2+( a0- b0) div b0 -1= q0+ 1+( a0- b0) div b0

pass comp

Теперь можно определить инвариант:

     X

    f(X)

   f(X0)

     a

(a – b) mod b

(a0 – b0 – b) mod b

     b

    b

  b0

     q

 q+(a – b) div b + 1

q0+(a0 – b0 – b) div b0 +2
Скачать файл