¿Existe alguna herramienta para la creación de prototipos de una semántica de lenguaje de programación y un sistema de tipos y que también permita algún tipo de verificación de modelo de propiedades estándar, como la solidez de tipo?
Pregunto esto, porque estoy leyendo un libro sobre Alloy y proporciona la funcionalidad exacta que quiero, pero para los modelos expresados con lógica relacional.
Soy consciente de Ott , pero no tiene este tipo de capacidad de "comprobación de modelo", ya que se centra en generar código para sistemas de asistente de prueba.
Cualquier referencia sobre la existencia de dicha herramienta sería buena.
reference-request
programming-languages
semantics
model-checking
Rodrigo Ribeiro
fuente
fuente
Respuestas:
Aunque existen marcos creados específicamente con el propósito de crear prototipos de lenguajes de programación (incluida su semántica, sistemas de tipos, evaluación, así como verificar propiedades sobre ellos), la mejor opción depende de su caso particular y necesidades específicas.
Dicho esto, hay varias alternativas (quizás no tan distintas) que podría tomar (que incluyen las que ya ha mencionado):
Tenga en cuenta que existe una compensación entre lo fácil que es usar el marco / herramienta (por ejemplo, tan fácil como presentar la definición en papel o en Latex) y cuán poderosos son los mecanismos para verificar las propiedades del lenguaje (por ejemplo, incrustar el el lenguaje en un probador de teoremas puede permitir verificar propiedades muy elaboradas).
[1] Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt y Robert Bruce Findler. Ejecute su investigación: sobre la efectividad de la mecanización ligera. POPL, 2012.
[2] Daniel Jackson. Aleación: una notación de modelado de objetos livianos. TOSEM, 2002.
[3] Greg Dennis, Felix Chang, Daniel Jackson. Verificación modular de código con SAT. ISSTA, 2006
[4] Sistema de gestión de pruebas formales Coq
[5] Razonamiento formal sobre los programas. Adam Chlipala, 2016
[6] Sistema automatizado Leon para verificar, reparar y sintetizar programas Scala funcionales
fuente