Сборник задач по курсу «Теория вычислительных процессов» (стр. 11 )

11. Требуется исследовать влияние ошибок в программах на проведение доказательства правильности. Для каждой из приведенных ниже ошибочных программ постарайтесь, как и выше, провести доказательство правильности и выявить те места, где доказательство не будет проходить. Обнаружив ошибку в доказательстве, найдите некоторые специфические значения для данных, при которых программа будет давать неверный ответ.

А. Предположим, что программа из упражнения 1 по ошибке записана следующим образом:

1) F(N)  ≡  IF  N = 1  ТНЕN  2
  ЕLSЕ  ОТНЕRWISЕ  F(N – 1)

2) F(N)  ≡  IF  N = 1  ТНЕN  1
  ЕLSЕ  ОТНЕRWISЕ  F(N – 1) + 1

3) F(N)  ≡  IF  N = 1  ТНЕN  1
  ЕLSЕ  ОТНЕRWISЕ  F(N – 1) + N – 1

Б. Представьте себе, что программа из упражнения 7 записана по ошибке следующим образом:

DELETE1 (X, L)  ≡  IF  L = NIL  ТНЕN  NIL
ЕLSЕ  IF  X = CAR (L)  ТНЕN  CDR (L)
ЕLSЕ ОТНЕRWISE  DELETE1 (X, CDR (L))

В. Представьте себе, что по ошибке программы из упражнения 9 записаны одним из следующих способов:

1) INT (L1, L2)  ≡  IF  L1 = NIL  ТНЕN  NIL
ЕLSЕ  ОТНЕRWISE  INT (CDR (L1), L2)

2) INT (L1, L2)  ≡  IF  L1 = NIL  ТНЕN  NIL
ЕLSЕ  IF  MEMBER (CAR (L1), L2)  ТНЕN
  СONS (CAR (L1), INT (CDR (L1), CDR (L2)))
ЕLSЕ ОТНЕRWISE  INT (CDR (L1), L2)

3) INT (L1, L2)  ≡  IF  L1 = NIL  ТНЕN  NIL
ЕLSЕ  IF  MEMBER (CAR (L1), L2)  ТНЕN
  СONS (CAR (L1), INT (CDR (L1), L2))
ЕLSЕ ОТНЕRWISE  INT (L1, L2)

4) UNION (L1, L2)  ≡  IF  L1 = NIL  ТНЕN NIL
ЕLSЕ  IF  MEMBER (CAR (L1), L2)  ТНЕN
       UNION (CDR (L1), L2))
ЕLSЕ ОТНЕRWISE  СONS (CAR (L1),
       UNION (CAR (L1), L2))

Приложение

Задание на итоговую самостоятельную работу
по теме «Доказательству правильности программ»

Вариант № 1

Доказать с помощью простой индукции, что для любого положительного n

2 + 4 + 6 + … + (2n – 2) + 2n  =  n(n + 1).

Доказать правильность блок-схемы программы, вычисляющей 2n

Указание: приписать индуктивные утверждения (о входных данных, о правильности, о конечности и инвариант цикла) точкам 1, 2 и 3. Доказать, что утверждение-инвариант действительно является инвариантом (для доказательства использовать простую индукцию). Из инварианта цикла и утверждения о конечности получить утверждение о правильности блок-схемы.

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

SUB ПРИМЕР( )        

M = CELLS (1, 1)        Указание: приписать индуктивные утверждения

N = CELLS (1, 2)        (о входных данных, о правильности, о конечности

I = 1:  J = M        и инвариант цикла) нужным точкам программы,

DO WHILE (I < N)        оформив в виде комментариев и доказать правиль-

  J = J⋅M        ность программы аналогично предыдущему случаю

  I = I + 1

LOOP

CELLS (1, 3) = J

END SUB

Написать аксиомы верификации для оператора языка VBA

{A1}        Указание: для облегчения работы необходимо

DO UNTIL C        изобразить соответствующий фрагмент блок-схемы

       S

LOOP

{A2}

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

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

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

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

Сформулируйте и запишите формализованное условие верификации на пути из точки 2 в точку 2 блок-схемы из задания 2.

Литература

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

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

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

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

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

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

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

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

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