2

I want to verify following code 

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)
}

Please help me how I can use Leon online system to verify the above code

Getting following compilation Error

10:Mutable variables (e.g. 'var x' instead of 'val x') require xlang desugaring

14:Mutating variables requires xlang desugaring

9:Mutable variables (e.g. 'var x' instead of 'val x') require xlang desugaring

13:Block expressions require xlang desugaring Mutating variables requires xlang desugaring

12:Block expressions require xlang desugaring While expressions require xlang desugaring

Tom
  • 904
  • 1
  • 7
  • 21
  • Simply paste it there, and you will get an error message. It's not valid code of course, as the top-level class or object is missing. – Madoc Mar 13 '16 at 14:04
  • Check the compilation error you got then.. – marstran Mar 13 '16 at 14:28
  • Getting following compilation Error 10:Mutable variables (e.g. 'var x' instead of 'val x') require xlang desugaring 14:Mutating variables requires xlang desugaring 9:Mutable variables (e.g. 'var x' instead of 'val x') require xlang desugaring 13:Block expressions require xlang desugaring Mutating variables requires xlang desugaring 12:Block expressions require xlang desugaring While expressions require xlang desugaring – Tom Mar 13 '16 at 14:45
  • @Tom Fix your code then. Or ask in a forum. But StackOverflow is not for fixing broken code. – Madoc Mar 13 '16 at 16:29
  • @Madoc The code is perfectly fine ..showing output in scala compiler ....it is not working in leon ....which is a verification loop ...its online version i am not able to verify above code – Tom Mar 14 '16 at 06:50

1 Answers1

2

The code that you pasted has a few other issues, I'll assume it's a copy/paste error since the errors you are reporting are different, but here the fixed version:

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)  
}

Of note, you were using an assignment in the ensuring clause, and you should not use return along with ensuring as Scala would just shortcut the ensuring and directly return from the function. In general, don't use return in Leon, and I'm going to also advise to not use return with Scala in most cases. Also you had a(a-1) which is not valid Scala code for a multiplication, you should have a*(a-1).

Now, about the --xlang option for Leon online. The code you are trying to verify relies on imperative programming (vars and loops) and the support in Leon for imperative programming comes from a module called xlang. Unfortunately, xlang support was desactivated from Leon Online, as it behaves quite poorly with the synthesis features of Leon. We are working on improving the xlang module so that it can be run along with the rest of the features of Leon. Hopefully this should happen eventually.

In the meantime, your only option, if you wish to verify programs using imperative features such as the above, is to run Leon from the command line with the --xlang option:

./leon --xlang Test.scala

You can find some documentation on how to install Leon on your system here: https://leon.epfl.ch/doc/installation.html

Regis Blanc
  • 549
  • 2
  • 5
  • Thanks a lot for detail explanation. It is working thanks a lot – Tom Mar 15 '16 at 03:57
  • Hi @Regis Blanc I tried the above program, if the postcondition we give is incorrect, Leon gives a counterexample quickly; if the postcondition is correct, it does not terminate. – Tom Mar 18 '16 at 08:10