The post has been translated automatically. Original language: Russian
One of the most useful aspects of formal verification is that it can not just report that a property is being violated, but show a specific case in which this happens.
In SJV, such a result is called a counterexample.
Let's say a rule is set for the function: after the call, the counter must increase exactly by the passed value. SJV checks all valid states and inputs in a given area.
If the rule is violated for at least one case, the system returns this case.
This is no longer an abstract "verification failed" message. You can see which function violated the condition, what data was at the input, what was the state of the program before execution and what it became after.
This approach greatly reduces the distance between proof and routine engineering work.
The developer does not have to manually guess why the formula turned out to be incorrect. A counterexample turns a formal check into a specific scenario that can be reproduced, studied, and corrected.
This is how SJV helped to find an error in the Sekura JS compiler: a formal check revealed a discrepancy between the required behavior and the machine code, and then showed the area where this discrepancy manifests itself.
It is important for us that formal verification is not a separate academic stage of development.
It should work like a regular engineering tool: either confirm a given property, or give the developer enough information to understand the cause of the violation.
Therefore, a good verification result is not only "everything is correct."
Sometimes it's much more useful to get an accurate answer to a question.: where exactly the program stops being correct.
Одна из самых полезных сторон формальной верификации — она может не просто сообщить, что свойство нарушается, а показать конкретный случай, в котором это происходит.
В SJV такой результат называется контрпримером.
Допустим, для функции задано правило: после вызова счётчик должен увеличиться ровно на переданное значение. SJV проверяет все допустимые состояния и входные данные в заданной области.
Если хотя бы для одного случая правило нарушается, система возвращает этот случай.
Это уже не абстрактное сообщение «проверка не пройдена». Можно увидеть, какая функция нарушила условие, какие данные были на входе, каким было состояние программы до выполнения и каким оно стало после.
Такой подход сильно сокращает расстояние между доказательством и обычной инженерной работой.
Разработчику не нужно вручную угадывать, почему формула оказалась неверной. Контрпример превращает формальную проверку в конкретный сценарий, который можно воспроизвести, изучить и исправить.
Именно так SJV помогла найти ошибку в компиляторе Sekura JS: формальная проверка обнаружила расхождение между требуемым поведением и машинным кодом, а затем показала область, в которой это расхождение проявляется.
Для нас важно, чтобы формальная верификация не была отдельным академическим этапом разработки.
Она должна работать как обычный инженерный инструмент: либо подтвердить заданное свойство, либо дать разработчику достаточно информации, чтобы понять причину нарушения.
Поэтому хороший результат проверки — это не только «всё верно».
Иногда гораздо полезнее получить точный ответ на вопрос: где именно программа перестаёт быть правильной.
Share
