1

レオンで次のプログラムを試しました

object Test10 {

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

}

結果 -- 成功

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 )

 }

結果 -- 失敗 (終了していません)

システムが生産できないのはなぜですか?誰かが私を導くことができますか?

4

1 に答える 1

2

2 番目のプログラムは実際にはそうではありませんvalid。この事後条件はn、オーバーフローのために の大きな値に対して正しくありません。合計がオーバーフローすると、式は成立しなくなります。

で置き換えIntてみてくださいBigInt。うまくいくかもしれません。この問題も非線形演算のため難しい問題です。

レオンは反例を探しているため (プログラムは ではないためvalid)、オーバーフローに到達するまで数式を展開する必要があるため、終了しません。もちろん、反例を見つけて報告するだけの方がよいのですが、これは Leon で使用されているアルゴリズムによる制限です。

最初のプログラムはvalid、オーバーフローが決してないためであることに注意してください。

于 2016-06-27T09:55:16.007 に答える