K est un cadre sémantique exécutable basé sur la réécriture dans lequel les langages de programmation, les systèmes de types et les outils d’analyse formelle peuvent être définis à l’aide de configurations, de calculs et de règles. Les configurations organisent l’état en unités appelées cellules, qui sont étiquetées et peuvent être imbriquées.Les calculs ont une signification de calcul en tant que structures de liste imbriquées spéciales séquentialisant les tâches de calcul, telles que des fragments de programme. Les calculs étendent la syntaxe abstraite du langage d’origine.Les règles K (réécriture) indiquent clairement les parties du terme dont elles ne se soucient que, en écriture seule, en lecture-écriture ou qui ne se soucient pas. Cela permet de définir des langages réellement simultanés, même en présence de partage. Les calculs sont comme tous les autres termes de l’environnement d’écriture : ils peuvent être appariés, déplacés d’un endroit à un autre, modifiés ou supprimés. Cela rend K adapté à la définition de fonctionnalités intensives en contrôle telles que la terminaison brusque, les exceptions ou l’appel / cc.
Aperçu
- Une présentation de diapositives vidéo d’aperçu de dix minutes.
- Un tutoriel vidéo de quatre-vingt-dix minutes, donné à ETAPS’16.
- Une interview de haut niveau sur la sémantique basée sur la réécriture (Wolfram Schulte interviewe Grigore Rosu à l’ICSE ’11.
- FAQ
Téléchargement de l’outil K
- Les binaires d’outils K fournis sont pris en charge sous Linux, OS X et Windows. D’autres plateformes peuvent ou peuvent ne pas fonctionner correctement. Nous accueillons favorablement les informations sur la facilité d’utilisation des plates-formes non prises en charge ou les bogues dans les plates-formes prises en charge.
- Essayez notre page de support de l’éditeur pour obtenir des liens vers K définitions de coloration syntaxique pour divers éditeurs /Es populaires. N’hésitez pas à contribuer.
- Le code source (Java) est disponible sur GitHub, où vous pouvez également signaler des bogues (veuillez le faire).
Apprenez K
- Faites le tutoriel K!
- Lisez quelques articles sur K sur le Laboratoire des systèmes formels (FSL).
- Documentation utilisateur
- Builtins
Liens
- Page web K et logique correspondante à l’UIUC (États-Unis).
- K Page web à l’UAIC (Roumanie).
- Page web de logique correspondante à l’UIUC (États-Unis).
- Canal de discussion en ligne pour K utilisateurs (Slack & Riot). C’est la façon recommandée de poser des questions sur K et d’interagir avec la communauté K.
- Stackoverflow pour les questions générales à la communauté des utilisateurs K (utilisez le canal ci-dessus si vous souhaitez des réponses rapides).
