Использование model finding при разработке компилятора

Chapel — язык программирования, созданный для упрощения параллельных вычислений.
Компилятор этого языка, Dyno, использует нетривиальную логику для разрешения имен: например для того, чтобы понять, что требуется вызывать — метод с именем foo или одноименную функцию.

В процессе реализации авторы компилятора придумали несколько ухищрений, основанных на битовых картах, которые оптимизируют многократный поиск по пространству имен. Но как показать, что этот подход всегда выдает корректные результаты?

Один из авторов рассказал в своем блоге, как решил использовать известный model finder Alloy 6 для моделирования возможных состояний и поиска контрпримера. Простая модель на Alloy позволила доказать, что исходный алгоритм был неверным, и существовали примеры программ, в которых происходило неверное разрешение имен.

Хороший аргумент за использование формальных методов. Особенно столь легковесных и простых в применении.

#digest