Тесты зелёные. Code review пройден. Статический анализ ничего не нашёл. Кажется, всё отлично. Но есть один интересный вопрос: действительно ли мы доказали, что функция делает то, что от неё требуется? Или только убедились, что она прошла те проверки, которые мы придумали? Вот здесь меня зацепили Frama-C + ACSL. Для C-функции можно сначала формально записать проверяемое свойство: /*@ assigns \nothing; ensures a >= b ==> \result == a; ensures a < b ==> \result == b; */ int max2(int a, int b); Читается почти без подготовки: если a ≥ b → результат равен a; если a < b → результат равен b. А потом появляется реализация: int max2(int a, int b) { return a >= b ? a : b; } И вопрос уже другой: «Можно ли доказать, что именно эта реализация выполняет записанное свойство?» Frama-C/WP превращает C-код и ACSL-спецификацию в математические утверждения, которые нужно доказать. А дальше — то, что мне нравится больше всего. Реализацию можно переписать. Оптимизировать. Заменить алгоритм. Если требуемое свойство осталось прежним, формальная спецификация тоже может остаться прежней. Новую реализацию снова проверяем относительно неё. То есть вместо: «новый код похож на старый?» можно спрашивать: «новый код всё ещё выполняет то, ради чего существует?» Вот здесь формальные методы становятся очень практичными. Особенно когда есть небольшой объём кода, которому система действительно должна доверять — trusted code base. KasperskyOS публично описывает связанную инженерную задачу: TCB стараются минимизировать, чтобы наиболее строгие и дорогие методы проверки можно было сосредоточить на небольшой части системы, критичной для информационной безопасности. Получается красивая цепочка: инженерное требование → формальная спецификация на ACSL → реализация на C → математическое утверждение → доказательство А под ней ещё и классическая математика. Для requires/ensures естественно возникает тройка Хоара: {P} f {Q} где P — предусловие, f — программа, Q — постусловие. А WP использует weakest precondition calculus. ACSL при этом я бы не называл просто «языком низкоуровневых требований». Точнее — это язык формальной спецификации C-программ. Но сама идея мне кажется очень сильной: между текстовым требованием и реализацией появляется машиночитаемое свойство, выполнение которого можно формально проверять. И вот здесь мне особенно интересно мнение практиков. Если бы вам дали реальный критичный C-модуль — как далеко вы бы пошли с формализацией? Отдельные критичные свойства? Контракты всех функций? Поведение модуля целиком? И где бы вы провели границу между тем, что стоит доказывать формально, и тем, что разумнее оставить тестированию? Особенно интересно мнение тех, кто применял Frama-C, ACSL или другие средства deductive verification на реальном коде: что вы формализовали и что оказалось действительно полезным? P.S. Я не утверждаю, что KasperskyOS использует Frama-C или ACSL. Публичного подтверждения этому я не нашёл. Мне интересна применимость подхода к публично описанной ими инженерной задаче.