Методы и средства инженерии программного обеспечения
Модель формального доказательства конкретности программы
Сущность формального доказательства заключается в преобразовании кода программы к логической структуре [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] массив целых ).
