里昂在线系统如何设置XLang，可以吗？

Question

我想验证以下代码

object Test {

    def test(a: Int): Int = {
      require(a > 0)

      var sum = 0
      var i = 0

      while(i < a) {
        sum = sum + i
        i = i + 1
      }

      return sum
    } ensuring(res => res=a(a-1)/2)
}

请教如何使用Leon在线系统验证以上代码

出现以下编译错误

10：可变变量（例如 'var x' 而不是 'val x'）需要 xlang 脱糖

14：改变变量需要 xlang 脱糖

9：可变变量（例如 'var x' 而不是 'val x'）需要 xlang 脱糖

13：块表达式需要 xlang 脱糖变异变量需要 xlang 脱糖

12:块表达式需要 xlang 脱糖而表达式需要 xlang 脱糖

Answer 1

您粘贴的代码还有一些其他问题，我假设这是一个 copy/paste 错误，因为您报告的错误不同，但这里是固定版本：

object Test {
  def test(a: Int): Int = ({
    require(a > 0)
    var sum = 0
    var i = 0
    while(i < a) {
      sum = sum + i
      i = i + 1
    }
    sum
  }) ensuring(res => res == a*(a-1)/2)  
}

值得注意的是，您在 ensuring 子句中使用了赋值，您不应将 return 与 ensuring 一起使用，因为 Scala 只会简化 ensuring 并直接从 return功能。一般来说，不要在 Leon 中使用 return，我也建议在大多数情况下不要在 Scala 中使用 return。另外你有 a(a-1) 这不是有效的 Scala 乘法代码，你应该有 a*(a-1).

现在，关于 Leon 在线的 --xlang 选项。您尝试验证的代码依赖于命令式编程（变量和循环），Leon 中对命令式编程的支持来自一个名为 xlang 的模块。不幸的是，xlang 支持已从 Leon Online 停用，因为它在 Leon 的综合功能下表现很差。我们正在努力改进 xlang 模块，以便它可以运行与 Leon 的其他功能一起使用。希望这最终会发生。

与此同时，如果您希望使用上述命令式功能验证程序，您唯一的选择是从命令行使用 --xlang 选项运行 Leon：

./leon --xlang Test.scala

您可以在此处找到有关如何在您的系统上安装 Leon 的一些文档：https://leon.epfl.ch/doc/installation.html

里昂在线系统如何设置XLang，可以吗？

How to set XLang in Leon online system,Is it possible?

scala

leon