Мне было так весело играть с TLA+ и Coyote (см. самое последнее ), что я решил продолжить сравнение некоторых других инструментов формальных методов. Есть ряд проектов, выходящих из Microsoft Research, и мы снова можем использовать задачу Розеттского камня (которую я приблизительно определяю как что-то, что — теоретически — легко переводить между разными языками, что позволяет вам больше сосредоточиться на разница в языках, чем содержание проблемы). Если вы являетесь экспертом в области..