Корректность комплексов программ



1) Конструктивная – корректность взаимоотношения компонент комплекса

2) Функциональная – соответствие функций комплекса функциям спецификации.

Эталоны и методы проверки корректности

Средства проверки корректности

Эталоны   Методы проверки
1) Формализованные правила: - описания алгоритмов - описания данных - описания модулей - описания комплексов « 1) - синтаксический контроль - семантический контроль - структурный контроль
2) Программные спецификации - модулей - данных - взаимодействия модулей « 2) - контроль полноты спецификации (валидация) - верификация
3) Тесты - статические - динамические « 3) - просмотр / инспекция кода - структурный и функциональный контроль

Способы формирования эталонных тестов

1) Применение аналитических выражений

2) Использование моделирования

3) Использование прежних вариантов тестирования подобных программ

Понятие верификации программы

Верификация – аналитическое исследование корректности программы по ее тексту на основе формально-логической системы установления соответствия между программой и ее спецификацией с помощью аппарата исчисления предикатов первого порядка. В конечном счете это вычисление истинности предиката от двух аргументов: программы и ее спецификации.

Для упрощения верификации разделяют две составляющих выполнения программы:

1) частичную корректность – удовлетворение входной и выходной спецификациям программы при условии ее успешно завершения

2) проверка завершенности программы – достижение выхода при заданных спецификацией входных данных

Основные задачи анализа корректности при верификации

1) частичная корректность при условии завершенности

2) частичная некорректность при условии завершенности

3) завершенность

4) незавершенность

5) тотальная корректность – частичная корректность и завершенность

6) некорректность – частичная некорректность или незавершенность

START P(x) Выходу оператора приписывают предусловие P(x), это допустимое множество значений входных данных
STOP Q(x, f(x)) Оператор, обеспечивающий завершение, входу которого приписывается выходной предикат, или постусловие, где f(x) – целевая функция выполнения программы (которая устанавливает связь между входными и выходными данными)
Pgrm Спецификация, которая задает набор индуктивных объявлений для каждой точки графа разреза управления

1) Свойство частичной корректности

- предикат завершенности программы

2) Свойство завершенности

3) Тотальная корректность

Есть ограничения на форму представления программ и операторов, для которых вычисляются предикаты.

Проверка 6 свойств корректности программ с определенными ограничениями осуществляется методом индуктивных утверждений, предложенных Флойдом.

Список литературы

https://studfiles.net
https://works.doklad.ru/view/7bOqlofhMVE.html
http://www.tadviser.ru
https://studopedia.org


 

Заключение

На этом занятии мы познакомились с основными этапами решения задач с помощью компьютера.

Основные этапы решения задачи на ПК:

- Нужно понять и отнести к какому классу принадлежит задача;
- Записать известные связи между исходными данными и результатами с помощью математических соотношений;
- Выбрать подходящий способ решения задачи;
- Построить алгоритм для решения задачи;
- Записать код, на основе алгоритма, на одном из языков программирования;
- Отладка и тестирование программы.


Дата добавления: 2018-11-24; просмотров: 401; Мы поможем в написании вашей работы!

Поделиться с друзьями:






Мы поможем в написании ваших работ!