Методы и средства инженерии программного обеспечения
Для установления пути выражения декомпозируются
Для установления пути выражения декомпозируются на множество неравенств. Если это множество содержит некоторые несовместимости, то путь нельзя установить. В случае совместимости множеств создается множество данных, которые будут использоваться во время символьного выполнения.
Символьное тестирование применяться при определении тестовых данных для проверки отдельных путей с использованием символьных значений для реальных. При этом входные значения обозначаются символами, а операторы выполняются с использованием элементарной алгебры. Выполнение заданного пути обычно включает условные переходы, символьные выражения, до которых входят как алгебраические, так и булевские конструкции.
С целью проведения статического анализа используется различные инструменты, которые позволяют исследовать структуру программы и определить виды ошибок в программе: невыполнимые коды, неинициализированные переменные, которыми хотят воспользоваться, инициализированные, но не использованные переменные и др.
Многие отказываются от формального доказательства. Это связано с тем, например, алгоритм пузырьковой сортировки намного более простой, чем его логическое описание и доказательство, а также программы обработки нечисловых данных могут быть более трудными для понимания логики, чем числовые. Техника доказательства, которая базируется на входных утверждениях для их трансформации в выходные логические правила еще не означает, что в программе нет ошибок, поскольку нельзя распознать ошибки в программах, в интерфейсах, спецификациях, в синтаксисе и семантике ЯП или в документации.
