Инструмент прототипирования семантики языка программирования

Существует ли какой-либо инструмент для создания прототипа семантики и системы типов языка программирования, который также позволяет выполнять некоторую проверку моделей стандартных свойств, например, правильности типа?

Я спрашиваю об этом, потому что я читаю книгу по Alloy, и она предоставляет именно ту функциональность, которая мне нужна, но для моделей, выраженных с использованием реляционной логики.

Я знаю Отта , но он не имеет такого рода возможности «модель проверки», так как она ориентирована на генерацию кода для доказательства систем ассистентов.

Любое упоминание о существовании такого инструмента было бы неплохо.

Хотя существуют платформы, созданные специально для создания прототипов языков программирования (включая их семантику, системы типов, оценку, а также проверку свойств о них), наилучший выбор зависит от вашего конкретного случая и конкретных потребностей.

С учетом вышесказанного, вы можете выбрать несколько (возможно, не столь внятных) альтернатив (включая те, которые вы уже упомянули):

• с использованием определенного языка / среды, предназначенной для создания и создания прототипов новых языков: например, Redex [1], предметно-ориентированный язык, встроенный в Racket, для определения и проверки (операционной) семантики языков программирования, который, учитывая определение язык, обеспечивает простую обработку таких задач, как набор текста (в латексе), проверка следов сокращения, юнит-тесты и случайное тестирование (например, для проверки набора текста)
• использование общих языков моделирования, которые позволяют легко определять и выполнять определенные анализы, при условии, что они могут охватить конкретный язык под рукой в ​​необходимой степени; Alloy [2] является примером такого подхода: хотя и довольно общий и гибкий, языки могут быть смоделированы как отношения между состояниями, в то время как поддержка проверки модели (например, оценка внутри такого языка) предоставляется бесплатно после того, как семантика выражена с помощью модель отношений (например, некоторые идеи для моделирования семантики языка можно найти в [3])
• встраивание языка для проверки его свойств с использованием средства доказательства теорем; пример будет определять язык, а также его семантику, встраивая его в систему доказательств, такую ​​как Coq [4] (более подробная информация об этом подходе, а также обсуждение и демонстрация различия между глубоким и неглубоким встраиванием в Coq приведены в [ 5])
• использование Ott (как уже упоминалось, по духу похожее на Redex, но обеспечивающее новый язык определения, а не встраиваемый); Отт позволяет вам определять язык программирования в удобной нотации и производить набор и определение типов в системе доказательств (обычно с глубоким встраиванием), где большая часть проверки (т.е. доказательство) должна выполняться вручную.
• разработка языка и его семантики, а также соответствующих проверок (например, тестов) «с нуля» на языке программирования общего назначения и, при необходимости, перевода в другие системы для целей проверки (в некоторых языках, таких как Leon [6], включает встроенные верификаторы, которые позволяют автоматически проверять определенные свойства и делают этот подход похожим на встраивание в систему доказательства)

Обратите внимание, что существует компромисс между тем, насколько просто использовать каркас / инструмент (например, так же просто, как выложить определение на бумаге или в латексе), и насколько мощными являются механизмы для проверки свойств языка (например, встраивание язык в доказательстве теорем может позволить проверить очень сложные свойства).

[1] Кейси Кляйн, Джон Клементс, Кристос Димулас, Карл Истлунд, Матиас Феллайзен, Мэтью Флэтт, Джей А. Маккарти, Джон Рафкинд, Сэм Тобин-Хохштадт и Роберт Брюс Финдлер. Проведите исследование: об эффективности облегченной механизации. ПОПЛ, 2012.

[2] Дэниел Джексон. Alloy: облегченная нотация для моделирования объектов. TOSEM, 2002.

[3] Грег Деннис, Феликс Чанг, Даниэль Джексон. Модульная проверка кода с помощью SAT. ISSTA, 2006

[4] Система формального доказательства Coq

[5] Формальные рассуждения о программах. Адам Чипала, 2016

[6] Леон автоматизированная система для проверки, восстановления и синтеза функциональных программ Scala