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

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

Согласно теореме об инвариантах, инвариант для f = [doguntilp od];  определяеться следующим равенством       q(X) = (f(X) = f ° g(X0))

1)  q+(a – b) div b + 1= q0+(a0 – b0 – b) div b0 +2;

 2)      b = b0;

          3)   (a – b) mod b = (a0 – b0 – b) mod b.

Эта система уравнений является искомым инвариантом, однако можно её несколько упростить. Из равенства (3) и (2) следует, что

(a – a0 + b0) mod b0 = 0, а из (1) равенства – (a – b) div b0 – (a0 – 2b0) div b0= q0 – q + 1. Тогда получим инвариант (a – a0 +b0 ) div b = q0 – q+1, поскольку (a – a0+b0 ) mod b0 = 0, то

(a – a0+b0 )  = b0* (q0 – q +1) - это и будет инвариант.

1) этот предикат верен перед выполнением цикла, т.к.  a = a0, а  q = q0;

2)  этот предикат выполняется во время выполнения цикла

                                        (( a0 – b0)- a0 +b) ) = b* (q0 +1 – (q0 +1));

3)  после выполнения цикла a < b, следовательно,  из равенства (1) получаем –

q = q0 +(a0 – b0 – b) div b0 +1  и из равенства (3) получаем (a – b) = (a0 – b0 – b0) mod b0   →  a = (a0 – b0 – b0) mod b0  + b0 → a = (a0 – b0 – b0 + b0) mod b0, а это есть предикат

q =q0  +( a0 – b0) div  b0 L  a=( a0 – b0) mod b0, что соответствует f ° g(X0).

Случай второй:

 преобразуем программу P1 в эквивалентную программу P2.

P2 = a,q := a – b,q + 1; while a ≥ b do a,q := a – b, q + 1 od

Докажем, что [P1] = [P2]. Регулярное выражение, соответствующее P1, будет выражение  (xy)+, если символом ‘x ‘ будем обозначать оператор a:= a – b, а символом ‘ y’ будем обозначать оператор q:= q + 1.

     Регулярное выражение соответствующее P2 – ( xy) (xy)* = (xy)+.

     Таким образом, программы P1 и P2 эквивалентны по выполнению и следовательно, эти программы эквивалентны функциональны. В этом случае достаточно доказать правильность программы P2.

Программа P2 не является элементарной программой. Следовательно, для доказательства её правильности необходимо выделить элементарные подпрограммы, из которых сконструирована программа P2.

P2 = a,q := a – b,q + 1; P‘2;

P‘2 = while a ≥ b do a,q := a – b, q + 1 od

Теперь рассмотрим подпрограмму P‘2. Определить программную функцию и инвариант для этолй программы: whilea ³ b doa, q:= a - b, q + 1 od.  Естественно, что с начала необходимо доказать правильность определённой функции, и только потом, используя эту функцию, строить инвариант для данной элементарной, циклической программы.

function (b, q,a - целые числа)

f=( a, b, q := a mod b, b, q+ a div b)

program

while a ³ b do a, q := a - b, q + 1od

proof

   term

Начальное значение a ³ b при каждой итерации уменьшается на b, так что в итоге

 while _ тест примет значение ложно

pass

while_test true ( доказать (p ® f)=(p ® f ° g))

фрагмент

условие

      a

       q

  a ³ b

a0 ³ b0

     a1=a0

q1=q0

a, q := a - b, q + 1

a2 = a1 - b0

q2 = q1+1

f=(a,b,q:=a mod b,b,q+a div b)

a3= a2 mod b0

q3= a2 div b0 + q2

выводы:

а) условие: a0 ³ b0

б) присваивание: a3 = a2modb0                        q3 = a2 div b0 + q2

                                  = (a1 - b0)mod b0                          =(a1 -b0)div b0 + q1+1

                                  = (a0 - b0)mod b0                          = (a0 -b0)div b0 + q0+1

                                  =a0 mod b0 - b0mod b0         =a0 div b0 -b0divb0+ q0+1

                                  = a0 mod b0                              = a0 div b0 - 1+ q0+1

                                                                                = a0 div b0 + q0

            

Функция программы:

f=( a0 ³ b0® a,b,q:=a0 mod b0, b0, q0+a0 div b0), которая при значении while _теста истина совпадает с заданной функцией.

pass

while_test false (доказать ( Ø p ® f ) = (Øp ® I))

(a < b ®( a,b,q:=a mod b,b,q+a div b)

Скачать файл