Даже верифицированный компилятор может допускать ошибки. В 2011 году исследователи тест...
Даже верифицированный компилятор может допускать ошибки. В 2011 году исследователи тестировали CompCert с использованием случайно сгенерированных C-программ и обнаружили ошибку "wrong-code" в следующем выражении: return -1 <= (1 && x); Правильный ответ — 1, но CompCert 1.6 для PowerPC выдал 0. Ошибка оказалась не в корректном оптимизаторе, а в неверифицированном фронтенде. Формальная верификация защищает только те части системы, для которых есть доказательства.
4 033 просмотров
Канал в каталоге MAXimeter
12 994 подписчиков · IT и технологии