ordering in postconditions affect verification results

[ChuyueSun]

Dafny version

4.0.0.50303

Code to produce this issue

method arrayProduct(a: array<int>, b: array<int>) returns (c: array<int>)
  // Precondition: Both arrays a and b are not null and have the same length.
  requires  a.Length == b.Length
  // Postcondition: The sequence of elements in c is the pair-wise product of the sequences of elements in a and b.
  ensures forall i :: 0 <= i < a.Length ==> c[i] == a[i]*b[i]
  ensures c.Length == a.Length  

{
  c:= new int[a.Length];
  var i:=0;
  while i<a.Length
    invariant 0<=i<=a.Length
    invariant forall j:: 0 <= j< i==> a[j] * b[j]==c[j]
  {
    c[i]:=a[i]*b[i];
    i:=i+1;
  }
}

Command to run and resulting output

dafny filename.dfy
filename.dfy(5,45): Error: index out of range
Dafny program verifier finished with 1 verified, 1 error

What happened?

But if I put " ensures c.Length == a.Length " before " ensures forall i :: 0 <= i < a.Length ==> c[i] == a[i]*b[i]", then verification is successful.

What type of operating system are you experiencing the problem on?

Linux

[fabiomadge]

I'd argue that it's just an implementation detail that the permutation fixes that check. Part of verification is checking the wellformedness of the specifications, which means, among other things, ensuring in-bounds array accesses, without taking the implementation into account. We do that linearly, and once a check passes, subsequent checks get to rely on the validated ones. This means that the order of clauses matters. I don't think improving on that, by doing some clever dependency analysis, is worth the effort.

If this is too hacky for your satisfaction, you can also ensure all clauses work independently, like I did here:

method M(a: nat) returns (c: array<bool>)
  ensures c.Length == a ==> forall i :: 0 <= i < a ==> c[i] || !c[I]
  ensures c.Length == a
{
  c := new bool[a];
}

[alex-chew]

This is a documented and intentional aspect of both ensures and requires clauses, so I don't think it's an implementation detail.

If more than one ensures clause is given, then the postcondition is the conjunction of all of the expressions from all of the ensures clauses, with a collected list of all the given Attributes. The order of conjunctions (and hence the order of ensures clauses with respect to each other) can be important: earlier conjuncts can set conditions that establish that later conjuncts are well-defined.

(https://dafny.org/dafny/DafnyRef/DafnyRef#sec-ensures-clause)

If more than one requires clause is given, then the precondition is the conjunction of all of the expressions from all of the requires clauses, with a collected list of all the given Attributes. The order of conjunctions (and hence the order of requires clauses with respect to each other) can be important: earlier conjuncts can set conditions that establish that later conjuncts are well-defined.

(https://dafny.org/dafny/DafnyRef/DafnyRef#sec-requires-clause)

[stefan-aws]

Another class of examples that demonstrates the relevance of the order of clauses is given by situations where one tries to call a partial function, thus need to establish its preconditions:

function F(n: nat): nat
  requires n != 0

function G(n: nat): nat

function H(n: nat): (m: nat)
  ensures G(n) != 0
  ensures m == F(G(n))

Arguably, the name conjunction is slightly confusing, as it typically is commutative.