CODEWITHSUNDEEP
dafny
Ben Reynwar
Ben Reynwar

Reputation: 1619

Dafny partial functions and "value does not satisfy the subset constraints" error

I'm trying to use partial functions for the first time, and am having trouble making sense of the error message.

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

This produces the error:

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

Any suggestions for what the problem is and how I can go about fixing it?

Update: I can resolve this error by adding a nat->nat subtraction function.

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

and then using that function in my lambda function.

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

I think what was happening is that the subtraction was producing an 'int' and then dafny was having trouble getting back to the 'nat'.

Upvotes: 0

Views: 68

Answers (1)

Mika&#235;l Mayer
Mika&#235;l Mayer

Reputation: 10711

It's because the closure you pass in argument has the type int --> int when the function it accepts is nat --> nat. nat is a subset of int, so it does not type check.

You might want to write this instead to force the types to be nat:

    ensures b_is_fa(a+offset, a, (x: nat) requires x >= offset => var r: nat := x - offset; r)

Upvotes: 1

Related Questions