Доказательство корректности

Реализация статической проверки динамических выражений AoRTE (“Absence of Run-Time Errors”), которая не даёт ложных срабатываний, хотя возможны ложные отрицательные результаты. То есть, если ошибки при компиляции отсутствуют, то можно быть уверенными, что проблем в коде нет, тогда как указание на возможную ошибку не всегда соответствует действительности и инструмент может ошибаться.

Формальный анализ не пытается доказать правильность программы в целом. Он используется только для доказательства определяемых пользователем утверждений в разных частях программы и вызовах функций. Причём доказательство правильности выполняется только в той мере, в какой это определено пользователем, а сами утверждения корректно и в полной мере описывают и ограничивают реализацию программы.

Формальный анализ доказательства корректности программы реализуется по принципу gnatprove для языка Ada и использует три макроса для определения предусловий, постусловий и утверждений: TRUST_ASSERT_PRED(), TRUST_ASSERT_POST() и TRUST_ASSERT() соответственно. Это среднее между assert и static_assert, которое выполняется во время компиляции программы, но в выражении могут использоваться неконстантные значения (неконстантные выражения должны быть вычислимы на уровне типов данных или описаны в пред- и постусловиях).