memory - 如何在 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 教程，可以在此处找到。