Составители:
Рубрика:
∀x(P(x) \/ ⎤Q(x)) ↔ ∀x(P(x) \/ ⎤Q(x)), где левая часть равна правой.
Следовательно, заданная формула является общезначимой.
2.6. Логика доказательства правильности
алгоритмов и программ
Цель данного раздела – познакомить читателя с принципами
верификации (доказательства правильности) алгоритмов и
программ. Создание и весь последующий жизненный цикл
надежного программного обеспечения для современных
информационно-вычислительных систем – многоэтапный и
трудоемкий процесс, который упрощенно можно охарактеризовать
как перевод требований технического задания сначала в точные
спецификации и, наконец, в текст программы.
Для описания алгоритмов используются различные методы,
отличающиеся степенью детализации и формализации.
Теоретическое описание обычно дается в повествовательно-
формальном изложении, цель которого – обосновать без лишних
подробностей процедуру, предлагаемую в качестве алгоритма. Для
наглядного представления структуры алгоритмов широко
применяются графические средства: графы, блок-схемы, сети.
Формальное и полное описание алгоритмов осуществляется на
алгоритмических языках; оно содержит всю необходимую для
реализации алгоритма информацию.
Сложность программного продукта как объекта
проектирования – основная причина ошибок перевода спецификаций
в текст программы и, следовательно, ненадежности программного
обеспечения. Для снижения сложности проекта используют
технологию модульного проектирования и объектно-
ориентированный подход.
Распространенный подход к обеспечению надежности
проектируемого программного обеспечения – это тестирование.
Цель тестирования – выявление ошибок, вкравшихся в программу на
111
Страницы
- « первая
- ‹ предыдущая
- …
- 25
- 26
- 27
- 28
- 29
- …
- следующая ›
- последняя »
