How to write semantics in K framework for a language similar to ada-spark

Question

I am working with K framework and trying to write semantics for a language similar to ada-spark and in that, I want to write semantics that involves allocation of memory and value when I declare an integer variable itself. Also

for the same approach, I tried to make a new cell but since the method to customize configuration is not given, hence I could not get a useful result.

Answer 1

In the K tutorial language SIMPLE, the semantics for allocating and initializing an integer variable looks something like this:

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

You can add new configuration cells to your language by adding them to the configuration declaration in your semantics.

For example, SIMPLE defines the following configuration:

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>

You may wish to refer to the entire K tutorial, which can be found here.