1

I have tried following programs in Leon

object Test10 {

     def sum(n: Int): Int = ({ 
        require(n >= 0)
        if (n == 0) 0
        else    sum(n-1)+1
    })ensuring(res => res==n )    

}

Result--Successful 

object Test10 {

     def sum(n: Int): Int = ({ 
        require(n >= 0)
        if (n == 0) 0
        else    sum(n-1)+n
    })ensuring(res => res==n*(n+1)/2 )

 }

Result--Failed(Not terminated)

Am I making any mistake,why the system is not able to produce?Can anyone guide me ?

Tom
  • 904
  • 1
  • 7
  • 21

1 Answers1

2

The second program is actually not valid. Ths postcondition is not correct for big values of n due to overflows. When the sum overflows, the formula will no longer hold.

You can try to replace Int by BigInt, it might work. The problem is also difficult due to non-linear arithmetic.

Leon is not terminating because it is looking for a counter-example (as the program is not valid) and has to unroll the formula until it reaches the overflow. Of course it would be better to just find the counter-example and report it, but this is a limitation due to the algorithm used in Leon.

Note that your first program is valid because there is never an overflow.

Regis Blanc
  • 549
  • 2
  • 5