Comments 2
Переменные х и у могут быть не инициализированы.Речь про строчку 21. Что-то я не понимаю: x — инициализируется строчкой выше, y — инициализируется в строке 9. Какие же они неинициализированные? И, собственно, интересно, про какие ошибки на 21 строчку сообщит Polyspace? Или не сообщит? Или это просто пример, который должен продемонстрировать сложность написания тестов? В общем, я что-то не понял, к чему всё это было.
0
Ну вот, вы провели статический анализ в голове и поняли, что переменные x и y на самом деле инициализированы (строчкой выше и на 9 строке). Но иногда такой анализ провести в голове не получается, и тогда вам помогает инструмент формальной верификации.
В зависимости от контекста, Polyspace отмечает определенные операции как надежные (доказанные) или как не надежные. Поэтому в этом конкретном случае Polyspace сообщит, что переменные являются инициализированными, укажет нам все возможные диапазоны этих переменных и сообщит, нет ли других проблем (например, переполнения или деления на ноль).
Механизм, который позволяет проводить такой анализ, называется «абстрактная интерпретация» и является процедурой формальной (математической) верификации — как описано в руководящих стандартах — например, DO-333.
В зависимости от контекста, Polyspace отмечает определенные операции как надежные (доказанные) или как не надежные. Поэтому в этом конкретном случае Polyspace сообщит, что переменные являются инициализированными, укажет нам все возможные диапазоны этих переменных и сообщит, нет ли других проблем (например, переполнения или деления на ноль).
Механизм, который позволяет проводить такой анализ, называется «абстрактная интерпретация» и является процедурой формальной (математической) верификации — как описано в руководящих стандартах — например, DO-333.
0
Sign up to leave a comment.
Всесторонний статический анализ с применением продуктов Polyspace