Как стать автором
Обновить

Всесторонний статический анализ с применением продуктов Polyspace

Время на прочтение 10 мин
Количество просмотров 2.7K
Всего голосов 3: ↑3 и ↓0 +3
Комментарии 2

Комментарии 2

Переменные х и у могут быть не инициализированы.
Речь про строчку 21. Что-то я не понимаю: x — инициализируется строчкой выше, y — инициализируется в строке 9. Какие же они неинициализированные? И, собственно, интересно, про какие ошибки на 21 строчку сообщит Polyspace? Или не сообщит? Или это просто пример, который должен продемонстрировать сложность написания тестов? В общем, я что-то не понял, к чему всё это было.
Ну вот, вы провели статический анализ в голове и поняли, что переменные x и y на самом деле инициализированы (строчкой выше и на 9 строке). Но иногда такой анализ провести в голове не получается, и тогда вам помогает инструмент формальной верификации.

В зависимости от контекста, Polyspace отмечает определенные операции как надежные (доказанные) или как не надежные. Поэтому в этом конкретном случае Polyspace сообщит, что переменные являются инициализированными, укажет нам все возможные диапазоны этих переменных и сообщит, нет ли других проблем (например, переполнения или деления на ноль).

Механизм, который позволяет проводить такой анализ, называется «абстрактная интерпретация» и является процедурой формальной (математической) верификации — как описано в руководящих стандартах — например, DO-333.
Зарегистрируйтесь на Хабре , чтобы оставить комментарий