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，我们使用这种机制来保存调用栈的列表。

---

针对评论进行了更新。

如果你想检查一个子项是否进行了状态转换，你可以把它改成这样（又是suedo代码）。

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>

注意这里我用了 "has reduced to sort Value"来确定它是否被 "评估"，当然你可以有任何你喜欢的侧面条件来确定。