0

考虑以下否定布尔值的复杂方法（取决于短路评估）：

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

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

4

1 回答 1

0

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

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

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

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

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

于 2015-05-26T12:20:54.843 回答