leon 中的短路评估 --xlang

Question

考虑以下对布尔值求反的复杂方法（取决于 short-circuit evaluation）：

def negate(a: Boolean) = {
  var b = true
  a && { b = false; true }
  b
} ensuring { res => res != a }

如果我在 Scala 控制台中测试这段代码，它会按预期工作。但是 leon --xlang 说后置条件无效。这是expected/specified吗？

Answer 1

查看 xlang 转换阶段后的（简化）编码，我们得到以下内容：

  def negate0(a0 : Boolean): Boolean = {
    val b1 = true
    val b2 = false
    b2
  } ensuring {
    res19 => res19 != a0
  }

第一个b1对应初始化var b = true。引入第二个b2对应赋值b = false。不幸的是，XLang 没有对 && 和 || 运算符进行任何特殊处理，这意味着它将提取子表达式中的所有副作用并将它们移动到 "top" 级别（因此你为什么有 val b2 = false)。最终返回值是 b2，最后一个已知的名字 b，显然表达式 a && ... 被忽略了（副作用除外）。

所以基本上这是 Leon 中的一个限制，我们将研究修复它。

编辑：请注意，这已在最新版本的 Leon 中修复：https://github.com/epfl-lara/leon/commit/2485477f4e91cba7fe6e0c137817d62f513a3c42

leon 中的短路评估 --xlang

short-circuit evaluation in leon --xlang

leon