K es un marco semántico ejecutable basado en reescritura en el que se pueden definir lenguajes de programación, sistemas tipográficos y herramientas de análisis formales mediante configuraciones, cálculos y reglas. Las configuraciones organizan el estado en unidades llamadas celdas, que están etiquetadas y pueden anidarse.Los cálculos tienen un significado computacional como estructuras de lista anidadas especiales que secuencian tareas computacionales, como fragmentos de programa. Los cálculos amplían la sintaxis abstracta del lenguaje original.Las reglas K (reescritura) hacen explícito qué partes del término solo leen, solo escriben, leen y escriben o no les importan. Este makesK es adecuado para definir lenguajes verdaderamente concurrentes incluso en la presencia de compartir. Los cálculos son como cualquier otro término en un entorno de escritura: se pueden comparar, mover de un lugar a otro, modificar o eliminar. Esto hace que K sea adecuado para definir funciones intensivas en control, como terminación abrupta, excepciones o llamada / cc.
Visión general
- Una presentación de diapositivas de vídeo de diez minutos de visión general.
- Un video tutorial de noventa minutos, dado en ETAPS ‘ 16.
- Una entrevista de alto nivel sobre semántica basada en reescritura (Wolfram Schulte entrevista a Grigore Rosu en ICSE’11.
- Preguntas frecuentes
Descarga de la herramienta K
- Los binarios de la herramienta K proporcionados son compatibles con Linux, OS X y Windows. Otras plataformas pueden o no funcionar correctamente. Agradecemos la información sobre la usabilidad de las plataformas no compatibles o los errores en las plataformas compatibles.
- Pruebe nuestra página de soporte para editores para encontrar enlaces a definiciones de resaltado de sintaxis K para varios editores/IDE populares. Por favor, siéntase libre de contribuir.
- El código fuente (Java) está disponible en GitHub, donde también puedes informar de errores (por favor, hazlo).
Aprende K
- ¡Haz el Tutorial K!
- Lea algunos artículos sobre K en el Laboratorio de Sistemas Formales (FSL).
- Documentación de usuario
- Builtins
Enlaces
- K y página web lógica correspondiente en UIUC (EE.
- Página web de K en UAIC (Rumania).
- Página web de lógica coincidente en UIUC (EE. UU.).
- Canal de discusión K en línea para usuarios de K (Slack & Riot). Esta es la forma recomendada de hacer preguntas sobre K e interactuar con la comunidad K.
- Stackoverflow para preguntas generales a la comunidad de usuarios de K (use el canal anterior si desea respuestas rápidas).
