kframework - 在 K 中的一系列整数上进行分支？

Question

我在文档中读到可以编写规则

syntax Exp ::= randBounded(Int, Int)
rule randBounded(M, N) => I
  requires M <=Int I andBool I <=Int N
  [unboundVariables(I)]

我想randBounded(4,6)返回一些随机整数。但是，当我尝试它时，它会返回一个整数V0并设置约束V0 <=Int 10 ==K true。

相反，有没有办法为范围内的每个整数生成显式分支？

例如，我想--search产生 3 种配置：每个整数 4、整数 5 和整数 6 一个。

Answer 1

不幸的是，您建议的扩展是不可能的，--search因此您无法获得确切的三种配置。但是，如果您实际上并不需要那些精确的配置，而是希望能够对它们的属性进行推理，那么使用此规则执行（符号）执行（使用 haskell 后端）以某种方式包含所有三种配置。