kframework - 上下文在 K 中究竟做了什么？

Question

K教程中简要提到了上下文的使用，作为自定义订单评估的一种方式。但我也看到了其他包含重写箭头的上下文语句，比如无类型简单语言中的这个。

context ++(HOLE => lvalue(HOLE))
rule <k> ++loc(L) => I +Int 1 ...</k>
     <store>... L |-> (I => I +Int 1) ...</store>  [increment]

有人可以解释一下上下文在 K 中是如何工作的吗？我特别感兴趣的是：

• 在 K 中是否有context比仅说明评估顺序更普遍的用法？
• context声明语句的顺序如何影响语义？

谢谢！

Answer 1

关于 K 中的上下文声明的更多详细信息可以在此处的 K 文档中找到。特别是，带有重写箭头的上下文意味着加热和冷却将用特定符号包裹要加热或冷却的术语。在您的示例中，该符号是lvalue.

具体回答您的问题：

• 上下文声明，如严格属性，主要用于指定评估策略。虽然理论上它们可以用于其他事情，但实际上这种情况很少发生。也就是说，评估策略可能很复杂，这就是为什么 K 具有与评估策略相关的许多不同特征的部分原因。在您提到的示例中，我们在上下文声明中使用重写，以便为评估左值提供一组单独的规则（即，避免实际评估一直到一个值，而只评估一个位置）。
• K 的句子是无序的。在单个模块中，您可以重新排序它的任何句子（除了 import 语句，它必须首先出现）并且不会对预期的语义产生影响（尽管如果您的语义是不确定的，后端可能会导致具体执行的行为略有不同）。这包括上下文声明。