结构操作语义在K？

Question

是否有规则的语法，如：

P => P'
-----------
P + Q => P'

或者我需要用计算上下文重新定义语义吗？

Kframework网站上有一本关于2010年以来的大步骤SOS的书，使用的是旧的语法：

crl < A1 / A2,Sigma > => < I1 /Int I2 >
if < A1,Sigma > => < I1 > /\ < A2,Sigma > => < I2 > /\ I2 =/= 0 .

它似乎做了我想要的，但我不确定是否存在新的语法。

Answer 1

您可以这样做(psuedocode)：

configuration <k> $PGM </k>
              <state> WHATEVER_YOUR_STATE_IS </state>

syntax KItem ::= evaluateInContext ( Exp , StateCell )
syntax Exp ::= Exp "/" Exp | "HOLE1" | "HOLE2" | Value
syntax Value ::= Int

rule <k> A1 / A2 => evaluateInContext(A1, <state> STATE </state>) ~> evaluateInContext(A2, <state> STATE </state>) ~> HOLE1 / HOLE2 ... </k>
     <state> STATE </state>

rule <k> evaluateInContext(A, <state> STATE </state>) => A ... </k>
     <state> _ => STATE </state>

rule <k> V:Value ~> evaluateInContext(A, S) => evaluateInContext(A, S) ~> V ... </k>

rule <k> V:Value ~> V':Value ~> HOLE1 / HOLE2 => V' /Int V ... </k>

所以你总是可以作为一流的公民来传递配置。

这方面的一个例子是在KEVM中，在这里我们使用这种机制来保存/检索一个调用堆栈列表。

更新以解决评论。

如果要检查子项是否进行状态转换，则可以将其更改为以下内容(再次使用psuedo代码)：

syntax KItem ::= "evaluated?" "(" Exp "," State ")" 
rule <k> evaluateInContext(A, <state> STATE </state>) => A ~> evaluated?(A, <state> STATE </state> ... </k>
     <state> _ => STATE </state>

rule <k> V:Value ~> evaluated?(A, <state> STATE </state>) => DO_SOMETHING_WHEN_EVALUATED ... </k>
rule <k> NOT_VALUE:Exp ~> evaluated?(A, <state> STATE </state>) => DO_SOMETHING_WHEN_NOT_EVALUATED ... </k>

请注意，我在这里使用“已降到排序Value”来确定它是否是“评估的”，但是您当然可以有确定它的任何附加条件。