Как написать семантику в K-фреймворке для языка, похожего на ada-spark

Question

Я работаю с K framework и пытаюсь написать семантику для языка, похожего на ada-spark, и в этом я хочу написать семантику, которая включает в себя выделение памяти и значения, когда я объявляю целочисленную переменную.Также

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

Answer 1

В языке учебника K SIMPLE семантика для выделения и инициализации целочисленной переменной выглядит примерно так:

  rule <k> var X:Id; => . ...</k>
       <env> Env => Env[X <- L] </env>
       <store>... .Map => L |-> undefined ...</store>
       <nextLoc> L => L +Int 1 </nextLoc>

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

Например, SIMPLE определяет следующую конфигурацию:

configuration <T color="red">
                <threads color="orange">
                  <thread multiplicity="*" color="yellow">
                    <k color="green"> $PGM:Stmts ~> execute </k>
                    <control color="cyan">
                      <fstack color="blue"> .List </fstack>
                      <xstack color="purple"> .List </xstack>
                    </control>
                    <env color="violet"> .Map </env>
                    <holds color="black"> .Map </holds>
                    <id color="pink"> 0 </id>
                  </thread>
                </threads>
                <genv color="pink"> .Map </genv>
                <store color="white"> .Map </store>
                <busy color="cyan"> .Set </busy>
                <terminated color="red"> .Set </terminated>
                <input color="magenta" stream="stdin"> .List </input>
                <output color="brown" stream="stdout"> .List </output>
                <nextLoc color="gray"> 0 </nextLoc>
              </T>

Вы можете обратиться ко всему учебнику K, который можно найти здесь .