Эти методы наиболее развиты, т.к. они относятся к области профессиональной деятельности программистов: кодирование, тестирование, отладка и др. Средства их проведения (решения) известны давно и динамически развиваются. Довольно хорошо формализованы методы определения спецификаций. Здесь уже имеется эффективная методология, хотя не все технические проблемы преодолены.
Верификация и испытания. Верификация и испытания занимают почти половину времени, отведенного на создание системы. Для уменьшения затрат, связанных с этими процессами, были разработаны средства отладки, представляющие собой специальные программы для проверки тех или иных характеристик системы. Самыми старыми и примитивными являются дамп и трассировка.
Дамп — это распечатка содержимого памяти. Однако поиск по дампу неэффективен, т.к. он выдается лишь по истечении некоторого времени после возникновения ошибки, так что причину последней установить достаточно трудно.
Трассировка — это анализ значения данных переменных после каждого выполнения оператора. В общем случае трассировка дает очень большой объем информации при минимальных пояснениях.
Анализаторы графов программы способны выявить ситуацию, когда либо происходит обращение к неинициированной переменной, либо после присвоения значения переменной к ней не обращаются.
Для тестирования программ используются генераторы тестовых данных. Проверка определенных условий в заданных точках осуществляется с помощью согласующих компиляторов. Для относительно простых языков разработаны системы автоматической верификации. В качестве примера средства, предназначенного для отработки этапов определения спецификаций и проектирования, можно назвать систему PSL/PSA.
Применительно к процессу разработки программного обеспечения термин «правильная» программа может иметь различную интерпретацию. Мы будем пользоваться восемью основными положениями. Правильная программа:
1) не содержит синтаксических ошибок;
2) не имеет ошибок, допущенных в процессе компилирования, либо сбоев в процессе выполнения;
3) для некоторых наборов тестовых данных обеспечивает получение правильного результата;
4) для типичных наборов тестовых данных обеспечивает получение правильного результата;
5) для усложненных наборов тестовых данных обеспечивает получение правильного результата;
6) для всех возможных наборов данных, удовлетворяющих спецификации задачи, обеспечивает получение правильного результата;
7) для всех возможных наборов данных и всех вероятных условий ошибочного входа обеспечивает получение правильного результата;
8) для всех возможных наборов данных обеспечивает получение правильного результата.
Естественно, что уровень правильности 8 не всегда достижим и, более того, не всегда необходим. Обычно для программных комплексов достаточно уровня правильности 6.
Достижение каждого уровня правильности требует затрат, и при проектировании комплекса разработчик сам должен обосновывать необходимый уровень правильности. Одним из путей, повышающих уровень «правильности» программ, является верификация. На настоящем уровне развития методов разработки полная автоматизация верификации невозможна.
Общим для различных систем верификации является представление программы в виде графа, с каждой дугой которого соотносится некоторый предикат (утверждение) (рис. 3.5).
Рис. 3.5 — Связь каждого оператора программы
с утверждениями Аi и Aj
Если Ai – входное утверждение, связанное с входной дугой оператора S, а Aj — утверждение, связанное с исходящей дугой того же оператора, тогда доказывается правильность оператора «если Ai истинно и оператор S выполнен, то утверждение Aj истинно». Подобный процесс может быть повторен для каждого оператора программы. Если A1 есть утверждение, предшествующее входному узлу графа (начальное утверждение), а An — утверждение на выходном узле, то «если A1 истинно и программа выполнена, то An истинно» (рис. 3.6).
Рис. 3.6 — Определение входа и выхода программы с помощью предикатов А1 и Аn
Подобный подход был формализован Хоором, который сформулировал ряд аксиом, определяющих влияние каждого типа операторов в языке на утверждение. Таким образом, доказательство правильности программ сводится к доказательству теорем исчисления предикатов.
Естественно, при таком математическом подходе результаты работы программы необходимо сравнивать с ее спецификациями. Каждая программа правильна лишь по отношению к некоторому набору спецификаций. Поэтому возникают вопросы:
· Эквивалентна ли спецификация предъявляемым к программе требованиям?
· Является ли программа правильной по отношению к этим спецификациям?
Это наиболее важные вопросы, которые мы будем решать при анализе правильности программ.