Методы и средства инженерии программного обеспечения


         

 Модель формального доказательства конкретности программы


Сущность формального доказательства заключается в преобразовании кода программы к  логической структуре [3, 6]  Составляется  описание  утверждений, которые задают вход–выход программ с помощью логических операторов, а также  комбинациями  логических переменных (true/false), логическими операциями (конъюнкция, дизъюнкция и др.)  и кванторами всеобщности и существования  (табл.7.1.).

                                                                                                                           Таблица 7.1       

                                  Логические операции                                            

       –––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––

            Название                         Примеры                        Значение

       ––––––––––––––––––––––––––––– ––––––––––––––––––––––––––––––––––––––––––

Конъюнкция                         x & y                           x  и  y

Дизъюнкция                          x * y                            x  или y 

Отрицание                             Øx                               не    x

Импликация                           x  ® y                        если

х то у

Эквивалентность                   х = у                           х

равнозначно у

Квантор всеобщности          " х Р(х)                      для всех  х, условие истинно

Квантор существования       $ х Р(х)                      существует х, для которого  

                                                                                         Р(х) истина

                        

     

1.  Для примера метода доказательства  предлагается к рассмотрению задача сортировки  одномерного массива  целых чисел Т длины N (Т [1:N]) для получения   из него эквивалентного массива Т’

той же длины N, что и Т,  элементы которого располагались бы  в порядке возрастания их  значений.

Входные условия  запишем  в виде  начального утверждения:

Аbeg:  (Т [1:N] – массив целых )  & ( Т' [1:N] массив целых ).       



Содержание  Назад  Вперед