使用Dafny偏函数时遇‘值不满足子集约束’错误的排查与解决

问题代码与错误提示 #

原代码尝试定义断言验证偏函数输出，并在引理中使用lambda偏函数：

predicate b_is_fa(a: nat, b: nat, f: nat-->nat)
    requires f.requires(a)
{
    b == f(a)
}

lemma checking(a: nat, offset: nat)
    ensures b_is_fa(a+offset, a, x requires x >= offset => x - offset)
{
}

运行后触发错误：

value does not satisfy the subset constraints of 'nat --> nat' (possible cause: it may have read effects)Verifier

错误原因 #

你的推测完全正确：Dafny中nat类型的减法操作x - offset会返回int类型——即便lambda的前置条件x >= offset能保证结果非负，Dafny的类型系统也不会自动将int隐式转换为nat。而断言b_is_fa要求第三个参数是nat-->nat类型的偏函数，返回值必须为nat，直接使用x - offset会导致类型不匹配，触发约束错误。

修复方案 #

显式定义一个返回nat类型的减法函数，通过前置条件确保输入满足非负结果要求，再在lambda中调用该函数：

定义nat减法函数 #

function sub(a: nat, b: nat): nat
    requires b <= a
{
    a - b
}

修改引理代码 #

lemma checking(a: nat, offset: nat)
    ensures b_is_fa(a+offset, a, x requires x >= offset => sub(x, offset))
{
}

此时lambda的返回值类型为nat，满足nat-->nat的类型约束，错误即可解决。

内容的提问来源于stack exchange，提问作者Ben Reynwar