1

是否有规则的语法，例如：

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

或者我是否需要使用评估上下文重新定义语义？

Kframework 网站上有一本关于 2010 年的 Big-Step SOS 的书，使用的是旧语法：

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

它似乎可以满足我的要求，但我不确定是否存在新的语法。

4

1 回答 1

1

你可以做这样的事情（伪代码）：

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

更新地址评论。

如果要检查子项是否进行了状态转换，可以将其更改为如下内容（再次伪代码）：

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”来确定它是否已“评估”，但您当然可以使用任何您喜欢的附带条件来确定它。

于 2020-04-30T19:51:55.377 回答