andrey

Путь к Файлу: /Таганрогский радиотехнический университет / Программирование Теория / PRAKT2.DOC

Ознакомиться или скачать весь учебный материал данного пользователя
Скачиваний:   0
Пользователь:   andrey
Добавлен:   24.01.2015
Размер:   763.5 КБ
СКАЧАТЬ

Основы теории верификации программ

Литература:

1. Е.А. Бутаков “Методы создания качественного ПО ЭВМ”, М.: Энергоиздат, 1984 (стр. 140-151)

2. Дал.У., Дейкстра Э., Хоф К. “Стуктурное программирование” М.: Мир, 1979.

 

Эпиграф:  

“Эксперементальное тестирование

 программ может служить доказательством

 наличия в них ошибок, но НИКОГДА

не докажет их отсутствия.”

Э. Дейкстра

 

Идея математического доказательства корректности программ (верификации) обычно сводится к докозательству того факта, что программа (подпрограмма) является корректной относительно ее входящей и выходящей спецификации. Правильность программы разделяется на 2 свойства: частичная корректность и оканчиваемость. Частична корректность подразумевает соответствие программы её спецификациям. Оканчиваемость означает, что программа закончится (т.е. не будет бесконечно “циклить”) при определенных входной спецификацией данных.

 

Наиболее известный метод

 

Метод Флойда доказательства частичной корректности программ

 

На основе операторных схем, называется методом индуктивных утверждений.

 

®

X  = (X1, ..., Xn) - входной вектор.

®

Y  = (Y1, ..., Yk) - программный  вектор, значения промежуточных результатов вычислений.

®

Z  = (Z1, ..., Zm) - выходной вектор.

Шаг 1

 

Разрезать циклы программы так, чтобы каждый цикл имел “точку разреза”. Сделать точки разреза на каждой дуге, исходящей из вершины “Пуск” и на каждой, ведущей в вершину “Останов”.

Пусть a - путь из точки разреза i к j (i=j - не исключается ). Ra (`X, Ra (`X,`Y )) -  предикат, определяющий условия, при которых исполнения программы идет по пути a , а функция  Za (`X,`Y )   - определяет преобразование вектора `Y  ( значение промежуточных результатов вычислениий) на этом пути. Ra  и Za  выражаются через функции и предикаты, встречающиеся на пути a.

 

Для  каждого пути b определить сообщение Rb  и Zb путем продвижения в обратном направлении по этому пути с следующими правилами подстановки:

PRAKT2a)

после подстановки PRAKT2

                  

                                                        до подстановки      PRAKT2

 

PRAKT2б) после подстановки PRAKT2

 

 

                                                      до подстановки       PRAKT2

                                                                                                          

f - некоторая функция отображающая X в Y.

g - некоторая функция , задающая значение программной переменной  `Y

 

PRAKT2после подстановки           PRAKT2

в) 

      до подстановки                        PRAKT2                                           

PRAKT2 г) после подстановки    PRAKT2

 

                                          до подстановки PRAKT2                                             

 

PRAKT2д) после подстановки PRAKT2

 

                 до подстановки  PRAKT2

 

PRAKT2Домашнее задание  Задача 1 для шага 1. Получить Ra и  ra для следуещего пути программы:

PRAKT2 решение

                                                                       PRAKT2

 

PRAKT2

 

PRAKT2                                 

 

PRAKT2                                                      

 

 

PRAKT2

Шаг 2

С каждой точкой разреза связывается предикат Pk (`X,`Y ), который называется индуктивным утверждением . Назначение этого предиката состоит в то, чтобы описать соотношение между переменными в этой точке. Это утверждение должно обладать тем свойством, что всякий раз, когда исполнение программы достигает точки k, Pk (`X,`Y ) должен быть истенным для текущих значений `X,`Y в этой точке. Кроме этого, входной предикат j (`X  ) связывается с начальной точкой разреза программы, а выходной  x (`X,`Z ) - с конечной. Этот шаг полнстью зависит от понимания алгоритма и его конкретной реализации.

 

Шаг 3

 Состоит в построении для каждого пути a, ведущего от точки разреза  i  к  j, верификационное условие:

 

"`X  "`Y [ ( Pi (`X,`Y ) Ù Ra (`X,`Y ) ) PRAKT2 Pj (`X, Za (`X,`Y ) ) ]                                                   ( 1 )

 

Это условие устанавливает, что если Pi (`X,`Y ) истинен для некоторых значений`X и`Y в точке i и эти значения таковы, что исполнение программы из точки i пойдет именно по пути a, то Pтоже истинен для значений `X и`Y в конце пути a ( точка  j ). В случае, когда  j - конечная точка, то:

 

"`X  "`Y [ ( Pi (`X,`Y ) Ù Ra (`X,`Y ) )    É  x  (`X, Za (`X,`Y ) ) ]                                                                ( 2 ) если   i - начальная, то 

 

"`X [ (j (`X ) Ù Ra (`X ) )    É Pj (`X, Za (`X  ) ) ]                                                                                                  ( 3 )

 

 

Шаг 4

Доказать все утверждения, получившиеся для разных путей по формулам  (1), (2) и (3).

(*)  Программа P  оканчивается модулем j, если для каждого входного вектора`x такого, что j (x) - истина, исполнение программы заканчивается.

Программа Р называется частично корректной относительно j  и x, если для j (x) º ТЛ  следует , что исполнение заканчивается  после исполнения Р:  x (`x, Р (`x ) ) -  тоже истинен.

Программа Р называется вполне корректной относительно j  и x, если для j (x) º Т  следует следует, что исполнение заканчивается и x (`x, Р (`x ) ) - истинен.

 

Задача 2                                                                                целого

Доказать правильность программы, вычисляющей  Z=[PRAKT2], " X ³ 0. Алгоритм приведен ниже и основан на том, что 1+3+5+...+ (2k+1) = (k+1)2    ," k ³ 0.

Значения  k  запоминаются в Y1,  нечетные числа 2k+1 - в Y3, и сумма  1+3+5+...+ (2k+1)  - в Y2.

Шаг 1

Надо доказать, что программа частично корректна относительно входного j(X) : X ³ 0 и выходного x(X,Z):  Z2 £  X £  (X +1)2   предикатов. Разрежим в точке В, получим 3 пути a ,b, g  (см. ниже).

PRAKT2
Шаг 2

j(X) и x(X,Z) уже введены.  Введем  предика для точки В:

Пусть это будет выражение: PRAKT2, полученное чисто при анализе алгоритма работы.

 

Путь PRAKT2

PRAKT2PRAKT2

 

PRAKT2

 

 

PRAKT2

 

 

 

Путь PRAKT2

PRAKT2PRAKT2

PRAKT2

 

PRAKT2

 

 

PRAKT2

 

Путь PRAKT2

PRAKT2PRAKT2

 

PRAKT2

PRAKT2

 

Шаг 3

Строим верификационные условия по формулам (1), (2), (3)

1) Для a :  PRAKT2 или 

PRAKT2

2) Для b:  PRAKT2 или

PRAKT2

3) Для  g:  PRAKT2 или

PRAKT2

 

Шаг 4

Проверка истинности условий

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

Т.к. PRAKT2, то PRAKT2. Далее

PRAKT2, наконец,

PRAKT2. Поэтому можно заключить, что программа Р является частично корректной относительно своих входного и выходного предикатов.

 

Задача 3

Доказать частичную корректность программы вычисления функции PRAKT2по приведенному алгоритму, для целого Х1 и натурального Х2.

Вычисление основано на соотношениях справедливых для любых PRAKT2 , причем  PRAKT2, еслиY2 - нечетное и PRAKT2, если Y2 - четное.

PRAKT2
Путь a : PRAKT2 1)

Путь b : PRAKT2 2)

Путь g : PRAKT2 3)

Путь d : PRAKT2 4)

 

1) PRAKT2 или PRAKT2.

2) PRAKT2 нечет. PRAKT2

                                          или

PRAKT2нечет PRAKT2

PRAKT2.

3) PRAKT2 чет. PRAKT2

                                      или

PRAKT2чет PRAKT2

PRAKT2.

4) PRAKT2 или PRAKT2.

 

 

 

Наверх страницы

Внимание! Не забудьте ознакомиться с остальными документами данного пользователя!

Соседние файлы в текущем каталоге:

На сайте уже 21970 файлов общим размером 9.9 ГБ.

Наш сайт представляет собой Сервис, где студенты самых различных специальностей могут делиться своей учебой. Для удобства организован онлайн просмотр содержимого самых разных форматов файлов с возможностью их скачивания. У нас можно найти курсовые и лабораторные работы, дипломные работы и диссертации, лекции и шпаргалки, учебники, чертежи, инструкции, пособия и методички - можно найти любые учебные материалы. Наш полезный сервис предназначен прежде всего для помощи студентам в учёбе, ведь разобраться с любым предметом всегда быстрее когда можно посмотреть примеры, ознакомится более углубленно по той или иной теме. Все материалы на сайте представлены для ознакомления и загружены самими пользователями. Учитесь с нами, учитесь на пятерки и становитесь самыми грамотными специалистами своей профессии.

Не нашли нужный документ? Воспользуйтесь поиском по содержимому всех файлов сайта:



Каждый день, проснувшись по утру, заходи на obmendoc.ru

Товарищ, не ленись - делись файлами и новому учись!

Яндекс.Метрика