kframework - 如何在 kframework 的一个规则中“要求”两件事？

Question

我想在一条规则中“要求”两件事。我写了类似的东西

rule left => right
  requires notBool(X in keys(A))
  requires notBool(L in keys(B))

但它不起作用。K 中有没有办法在一个规则上设置多个约束？

Answer 1

您需要使用布尔值和运算符分隔布尔条件，我们将其写为 andBool. 以下应该有效：

rule left => right
  requires notBool(X in keys(A))
   andBool notBool(L in keys(B))