如何在 K 框架中为类似于 ada-spark 的语言编写语义

Question

我正在使用 K 框架并尝试为类似于 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 教程，可以在 here 找到。