Type of - inferred to be nat

[RustanLeino]

The type of an integer-subtraction expression should never be inferred to be a subset type, but should be the base type thereof. This is not done properly, which causes the verifier to give an error in the following program:

method M(N: nat) {
  var i := N;
  while i != 0
    invariant i - 1 == i - 1 // error reported: result of operation may not be a 'nat'
  {
    i := i - 1;
  }
}

While it is true that the result of i - 1 above may not be a nat, this property should not have been checked in the first place.

Workaround: change i - 1 to i as int - 1

[DavePearce]

The type of an integer-subtraction expression should never be inferred to be a subset type

But, if you don't do that then the subsequent statement i := i - 1 won't type check? In Whiley I resolve this by forward propagating type information. Then we know that i - 1 in i := i - 1 is expected to be a nat whilst i-1 in i - 1 == i - 1 doesn't have to be.

[RustanLeino]

Here's another example, using the more innocently known operator +:

type EvenUpTo100 = x | x % 2 == 0 && x <= 100

method P(N: EvenUpTo100) {
  var i := N;
  while i != 100
    invariant i + 1 == i + 1 // error reported: result of operation may not be an 'EvenUpTo100'
  {
    i := i + 2;
  }
}

It seems we'd like to specify the type of the numeric + and - (and similar operators) as

A * B --> C

where A, B, and C are any numeric types where C is a supertype of both A and B and C is (this is the new constraint, which the type inference engine doesn't currently know about) a base type.

[RustanLeino]

@DavePearce If i has type nat and i - 1 is inferred to have type int, then Dafny would still allow the assignment i := i - 1, provided the verifier can prove that i - 1 is a nat at the time of assignment.

[DavePearce]

Hey @RustanLeino,

So basically you're doing a form of type inference where constraints are checked by the verifier? That sounds similar to Whiley then!

[RustanLeino]

Technically, the desired types are inferred by a more standard type-inference engine. Then, whenever there are conditions to be validated, they are part of what gets passed to the verifier. So, in Dafny and unlike Whiley (I think), the output of the verifier does not affect what types are inferred.