alloy4中一组实用/自然数的求和

Question

我发现自己在试图总结一套自然的东西。在运行一个简单的模型时，我对下面的行为感到困惑。

(假设以下代码位于util/自然科学的副本中，因此将导入ord )

//sums the values in a set of naturals
fun setsum[nums : set Natural] : lone Natural {
    {n : Natural | #ord/prevs[n] = (sum x : nums | #ord/prevs[x])}
}

然后，在一个模块中导入util/自然科学的副本：

private open mynatural as nat

let two = nat/add[nat/One, nat/One]
let three = nat/add[two, nat/One]
let four = nat/add[two, two]
let five  = nat/add[four,nat/One]

pred showExpectSum10 {
    some x : Natural | x in setsum[{n : Natural | nat/lt[n, five]}]
}

//run showExpectSum10 for 15 //result is 10, as expected
//run showExpectSum10 for 1 but 20 Natural //result is 10  as expected
run showExpectSum10 for 1 but 40 Natural //result is 26 somehow.

为什么改变自然的范围会这样影响结果呢？

Answer 1

似乎您只需要禁用溢出(“选项->禁止溢出:是”)，然后它就会像预期的那样工作。每次使用整数算法并允许溢出(这是默认设置)时，都可以得到虚假的反例(即无效实例)，这是由于合金中算术操作的默认“环绕”语义造成的。