When Dafny infers type nat for a value it does not automatically know the value is non-negative

Jul 16, 2014 at 2:38 PM
I have a function with a parameter of type nat which is decreased on recursive calls. Dafny can automatically verify termination, so all well and good there. However, I have noticed that when I introduce a value using a quatifier which I then use as the parameter to this function, if I don't explicitly state that the value of the type is nat, then Dafny complains that the value must be non-negative.

We can take the following as an example (http://rise4fun.com/Dafny/5O9j):
function Fact(n : nat) : nat
{
  if (n == 0) then
    1
  else
    n * Fact(n-1)
}

predicate ShouldVerify()
{
  exists n :: Fact(n) > 6
}

predicate DoesVerify()
{
  exists n : nat :: Fact(n) > 6
}
Would it not make sense for Dafny, whenever it infers that some value has type nat, also infer that it's value is non-negative? Or are there some subtleties I am missing?
Developer
Aug 21, 2014 at 5:29 PM
Dafny does not (for now) infer subrange types (ie nat), so the n in ShouldVerify will be an int.
The expression exists n :: int :: Fact(n) > 6 will then fail the well-formedness check, because some unbounded integer n is being applied to Fact. This check happens before we even try to find a witness to the existential.
Marked as answer by rustanleino on 9/9/2014 at 1:56 PM
Coordinator
Sep 9, 2014 at 10:17 PM
It would be tricky for type inference to decide if you want all of int or just the subrange nat. The difference plays a role exactly in quantifications, as you have found. For example, what would you say should be the type of x in:
forall x :: if P(x) then 1000 <= Fact(x) else 0 <= x
where
predicate P(y: int)
{
  100 <= y
}
function Fact(n: nat): nat
{
  ...  // as above
}
If x is inferred as int, the value of the forall expression is false, whereas if x is inferred as the subrange nat, then the forall expression would be true.

Here's an even simpler example:
forall x :: 0 <= x
What should be the type of x, int or nat?

It is for this reason that Dafny does not infer types of quantified variables to be subrange types.

If you wonder about what type has been inferred for a variable, just hover over the name of the variable in the Dafny IDE in Visual Studio and the hover text will tell you.

Rustan