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

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

       = (a < b ®a,b,q:=a,b,q+0)

        = (a < b ®a,b,q:=a,b,q)

т.е. получили тождественную функцию, что и требовалось доказать

pass

result

pass comp

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

     X

    f(X)

   f(X0)

     a

 a mod b

a0 mod b0

     b

    b

  b0

     q

 q+a div b

q0+a0 div b0

Согласно теореме об инвариантах,  для построения инварианта необходимо приравнять компоненты, соответствующие f(X) и f(X0):

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

 2)      b = b0;

3)   a mod b = a0 mod b0.

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

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

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

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

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

6)  после выполнения цикла a < b, следовательно,  из равенства (1) получаем -  a0 div b0 = q  - q0  и из равенства (3) – a = a0 mod b0, а это есть предикат q = a0 div  b0+q0 L  a= a0 mod b0, что соответствует функции программы.

Далее продолжим доказательство. В программе  P2 = a,q := a – b,q + 1; P‘2; заменяем подпрограмму P‘2 на её функецию и получаем новую программу

                 ( P‘’2  = a,q:= a – b,q + 1;  a,b,q := a  mod b,b,q + a div b;), которая является уже линейной программой и доказывается следующим образом:

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

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

a,q := a – b,q + 1;  a,b,q := a  mod b,b,q + a div b;

proof

f =[g;h] = h◦g

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

pass comp

4.5.3 Полные и ограниченные инварианты

Если рассмотреть цикл типа while _do,то отношение

 q(X)=(f(X)=f(X0)) - называется полным инвариантом цикла while_do, а для любого инициированного циклаh; whilepdogod отношение q(X)=(f(X)=f ° h(X0)) - называется ограниченный инвариант цикла while_do. Заметим, что ограниченный инвариант цикла while_do совпадает с инвариантом цикла do_until ( см. теорему об инварианте).

Инициирование программы типа while_do ограничивает её применение подмножеством функций while_do. В результате ограниченный инвариант будет проще, чем полный инвариант while_do.

 Например, для программы P2:

a,q := a – b,q + 1; while a ³ b doa, q := a - b, q + 1 odс функцией:

f = (a, b, q := a mod b, b, q+ a div b) ограниченный инвариант:

     X

    f(X)

 f ° h (X0)

     a

 a mod b

(a0 – b0) mod b0

     b

    b

  b0

     q

 q+a div b

q0 + 1 + (a0- b0) div b0

q+a div b = q0 + 1 + (a0- b0) div b0

         b = b0

   a mod b = (a0 – b0) mod b0 приводим данную систему к общему инварианту, так же как при выводе полного инварианта и получаем:

(a – a0 +b0 )  = b*(q0 – q +1) - ограниченный инвариант.

         5. МЕТОДИЧЕСКИЕ УКАЗАНИЯ К ВЫПОЛНЕНИЮ РАССЧЁТНО – ГРАФИЧЕСКОЙ РАБОТЫ (РГР)

Цель: контроль знаний, полученных студентами при самостоятельном изучении материала: программа как математический объект.

РГР включает четыре задания :

1 тема: проектирование программы и разработка полного набора тестов;

2 тема: верификация программы на основе теоремы правильности;

3 тема: разработка инвариантов для циклических элементарных программ;

4 тема: анализ и структурирование схемы – программы.

5.1 Проектирование программы

Цель: научиться анализировать поставленную задачу и как результат анализа,  уметь разработать проект решения, описав его на PDL, или  разработанный проект представить в виде конечного автомата. Кроме того,  уметь  показать правильность проектного решения, предложив полный набор тестов.

Скачать файл