Основные этапы процесса разработки программ
Процесс разработки программы может быть разбит на два основных этапа:
Разработка программы начинается с анализа и формулирования требований к программе, с разработки точного описания того, чего нужно достичь в результате работы программы и в каком виде будет представлен нужный результат.
Далее выбирается технология программирования, с использованием которой будет разрабатываться программы (например, структурное программирование).
Полученный вариант разработанной программы подвергается систематическому тестированию на наличие ошибок, что является вполне нормальным закономерным явлением для новых программ. Практически невозможно написать реальную (достаточно сложную) программу с первого раза без каких-либо ошибок.
Статья: Основные этапы процесса разработки программ. Контроль текста программы до выхода на компьютер
После исправления таких ошибок программа подвергается дальнейшей проверке на правильность выдаваемых результатов. Ведь то, что программа в результате своей работы выдала какой-то результат, еще не означает, что этот результат – правильный. Для проверки правильности результатов программа подвергается проверке на наличие логических ошибок в решении задачи. Ответственные участки программы проверяются с использованием методов доказательства правильности программ.
Методы доказательства правильности программ
Неформальными методами доказательства правильности программ является отладка и тестирование – необходимые составляющие на всех этапах процесса программирования. Но эти методы не решают полностью проблему правильности программы. Существенные ошибки легко можно найти при использовании соответствующих приемов отладки (контрольных распечаток, трассировок).
Программу считают правильной, если она решает сформулированную задачу.
Метод установления правильности программ при помощи строгих средств называется верификацией программ.
При тестировании программ проводится анализ свойств отдельных процессов выполнения программы, а при верификации анализируются свойства программ.
Метод верификации основывается на предположении, что существует программная документация, соответствие которой требуется доказать. В документацию должны входить:
- спецификация ввода-вывода (описание данных, которые не зависят от процесса обработки);
- спецификация структур данных, которые зависят от процесса обработки;
- свойства отношений между элементами векторов состояний в выбранных точках программы;
- спецификации и свойства структурных подкомпонентов программы.
К методам доказательства правильности программ относится метод индуктивных утверждений, который сформулировал независимо друг от друга К. Флойд и П. Наур.
Суть метода индуктивных утверждений:
- формулировка входного (описание всех необходимых входных условий) и выходного (описание ожидаемого результата) утверждения;
- принимается истинность входного утверждения, создается промежуточное утверждение (выведенное утверждение), которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями);
- формулировка теоремы (условие верификации):
- из выведенного утверждения следует выходное утверждение;
- доказательство теоремы, которое показывает правильность программы (или программного фрагмента).
Доказательство проводится с помощью математических методов, которые используют исчисление предикатов I-го порядка.
Условия верификации можно строить и в обратном направлении: принимая истинность выходного утверждения, получить входное утверждение и доказывать теорему: из входного утверждения следует выведенное утверждение.
С помощью индуктивных утверждений можно формализовать интуитивные представления о логике программы, что является самым сложным в процессе доказательства правильности программы.
Для доказательства завершения выполнения программы часто достаточными являются неформальные рассуждения. Алгоритм доказательства правильности программы методом индуктивных утверждений:
Этот метод можно сравнить с обычным чтением текста программы (методом сквозного контроля) с разницей лишь в степени формализации.
Преимуществом верификации является возможность формализации процесса доказательства, что позволяет выполнять его на вычислительной машине.
Общим свойством перечисленных методов является то, что они рассматривают программу как уже существующий объект и затем доказывают ее правильность.
Метод, сформулированный К. Хоаром и Э. Дейкстра, основывается на формальном выводе программ из математической постановки задачи.
Каждая программа обязательно подвергается анализу обеспечения качества и эффективности программного обеспечения, проводится анализ и улучшение временных характеристик.
Контроль текста программы до выхода на компьютер
Текст программы можно контролировать за столом следующими методами:
- Просмотр. Текст программы просматривается с целью проверки на описки и расхождения с алгоритмом. Просматривается организация всех циклов с целью проверки правильности операторов, которые задают кратности циклов. Полезно провести проверку условий в условных операторах, аргументов в обращениях к подпрограммам и т.п.
- Проверка. По тексту программы программист восстанавливает вычислительный процесс, который проводит программа, и сверяет его с требуемым процессом.
- Прокрутка – имитация программистом за столом выполнения программы на машине. Достаточно трудоемкий процесс, который зачастую применяется только при контроле логически сложных участков программы. При выполнении прокрутки задают исходные данные и производят над ними необходимые вычисления. Исходные данные должны быть выбраны так, чтобы в прокрутку вовлекалось большинство ветвей программы.
