Курсовая работа по «Теории вычислительных процессов»

3. Доказать правильность программы, написанной на VBA.

 

SUB ПРИМЕР( )

M = CELLS (1, 1)

N = CELLS (1, 2)

‘M,N – целые значения

‘N ³ 1

I = 1:  J = M

DO WHILE (I < N)

`J = M ^ I – инвариант цикла

‘I = N – условие конечности

   J = J × M

   I = I + 1

LOOP

CELLS (1, 3) = J

‘J = M ^ N

END SUB

Сначала необходимо доказать конечность программы, для  этого необходимо показать, что в  конце концов мы выйдем из единственного  в программе цикла. Для этого  нужно доказать, что проверка I < N, управляющая циклом, даст отрицательный результат. Так как значение I в каждой итерации цикла увеличивается на 1,а N ³ 1 и не меняется в программе, то рано или поздно I станет равным N, а значит условие I < N станет ложным и мы выйдем из цикла, т.е. программа завершится.

1. Путь от метки 1 до метки 2. Предположим, что только что были считаны переменные и справедливо выражение, записанное сразу после метки. Теперь последовательно выполняются операторы до метки 2. Утверждение, записанное после метки 2 будет справедливым, так как мы имеем I = 1 и J = M, значит J = M ^ 1 = M ^ I.

2. Путь от метки 2 к метке 3, и снова к метке 2 (т.е. тело цикла).

Предположим, мы выполняем оператор 2 и справедливо  записанное после него утверждение, затем выполняем цикл и возвращаемся к метке 2. Необходимо показать, что  указанное утверждение будет  снова справедливо.

Пусть I и J в этой точке принимают значения I_n и J_n, т.е. J_n = M ^ I_n. При возвращении в точку 2 I и J принимают новые значения I_n+1 и J_n+1, которые можно представить следующим образом:

I_n+1 = I_n + 1,

J _n+1 = M * J_n = M * M ^ I_n = M ^ (I_n + 1) = M ^ I_n+1

                                            (так как J_n = M ^ I_n)

Следовательно, при очередном попадании в  точку 2 высказывание

J = M ^ I вновь справедливо, что и требовалось доказать, т.е. при любом попадании в точку 2 справедливо высказывание J = M ^ I.

3. Путь от оператора 2 к оператору 4. Предположим, что мы выполнили оператор 2, справедливо соответствующее утверждение и переходим к оператору 4. Нужно показать, что справедливо утверждение, записанное ниже этого оператора. Оператор 2 передаст управление на оператор 4 только при отрицательном результате проверки I < N,

т.е. при I = N. При переходе от оператора 2 к оператору 4 ни одно из значений переменных не изменяется, и, следовательно, при достижении метки 4 мы имеем J = M ^ I = M ^ N. Таким образом, мы доказали правильность программы.

 

4. Доказать правильность рекурсивной  программы методом структурной  индукции (для положительных значений  аргумента N)

 

F(2N)  º  IF N = 1 THEN 2

ELSE  OTHERWISE   2N + F(2N –2)

Гипотеза: F(2N) = N(N+1)

Нужно доказать, что F(2N) = N(N+1)для любого положительного числа N. При доказательстве с помощью структурной индукции используем простую индукцию по положительным целым числам:

1. Докажем, что F(2*1) = 1(1+1). Действительно, F(2*1) = 2 = 1*2.

2. Докажем (для любых положительных N), что если F(2N) = N(N+1), то F(2(N+1)) = (N+1)(N+2). Так как N положительное число, то проверка N+1 = 1 дает отрицательный результат, а потому получаем:

F(2(N+1))=2(N+1)+F(2(N+1)-2)=2(N+1)+F(2N)=2(N+1)+N(N+1)=(N+1)(N+2)

                                                                                                                            (по гипотезе индукции)

что и требовалось доказать, т.е. F(2N) = N(N+1) для любого положительного N.

 

 

Список использованной литературы

1. Веретельникова Е.Л. Доказательство правильности программ: Метод индуктивных утверждений. Конспект лекций. – Новосибирск, Изд-во НГТУ, 2004. – 59 с.

2. Веретельникова Е.Л. Доказательство правильности программ: Дополнительные приемы. Конспект лекций. – Новосибирск, Изд-во НГТУ, 2005. – 36 с.

3. Андерсен  Р. Доказательство правильности  программ. – М.: Мир, 1982. – 163 с.

4. Информатика.  Теория и практика структурного  программирования: Методическая разработка. – Новосибирск, изд-во НГТУ, 1999.

5. Лингер Р., Миллс Х., Уитт Б. Теория и практика структурного программирования. / Пер. с англ., М.: Мир, 1982.

6. Хопкрофт Дж., Мотвани Р., Нильман Дж. Введение в теорию автоматов, языков и вычислений, 2-е изд. – М.: Изд. дом «Вильямс», 2002.

7. Метод  индуктивных утверждений для  доказательства правильности программ: Учебное пособие. – Новосибирск, 2002. – В электронном виде.

8. Кнут  Д. Искусство программирования  для ЭВМ. – М.: «Мир», Т. 1, 1976.

9. Романов  Е.Л. Практикум по программированию  на С++: Уч. пособие. СПб: БХВ-Петербург;  Новосибирск: Изд-во НГТУ, 2004. –  432 с.

 

Размещено на Allbest.ru