what is wrong with postcondition in Dafny?

user_13042987 0
Viewed 100
function sumTo( a:array<int>, k:int, j:int)  : int
  requires a != null;
  requires 0 <= k && k <=a.Length;
  requires k <= j && j <= a.Length-1;
  decreases j;
  reads a;
{
  if (k == j) then a[k] else sumTo(a, k, j-1) + a[j]
}

method prod(t:array<int>)  modifies t
requires t!=null  && t.Length>=2
ensures forall k: int :: 0 <= k < t.Length ==> t[k]== sumTo(old(t), k, t.Length-1)
{
    
    var i := t.Length - 2;
    while i>=0
        invariant t.Length-1>i>=-1;
        decreases i;
    {
        t[i] := t[i]+t[i+1];
        i := i-1;
    }

}

returns this error :

  • web.dfy(17,4): Error BP5003: A postcondition might not hold on this return path.

  • web.dfy(13,8): Related location: This is the postcondition that might not hold.

dafny
1 Answers

Right, I did manage to solve this in the end though changed sumTo() to make it easier (specifically operating over sequences rather than arrays). Here's how it looks:

function sumTo(a:seq<int>, k:int)  : int
requires 0 ≤ k ∧ k < |a|;
decreases |a| - k;
{
  if (k+1) == |a| then a[k]
  else a[k] + sumTo(a,k+1)
}

method prod(t:array<int>)
  modifies t;
  requires t.Length ≥ 2;
  ensures ∀ k: int ∙ 0 ≤ k < t.Length ⟹ t[k]== sumTo(old(t[..]), k)
{

    var i ≔ t.Length - 2;
    while i ≥ 0
      invariant -1 ≤ i < t.Length - 1;
      // Last element unchanged
      invariant t[t.Length-1] == old(t[t.Length-1]);
      // Everything upto (and including) ith element unchanged
      invariant ∀ k:int ∙ 0 ≤ k ≤ i ⟹  t[k] == old(t[k]);
      // Everything else matches the sum we want
      invariant ∀ k:int ∙ i < k ∧ k < t.Length ⟹  t[k] == sumTo(old(t[..]), k);
    {
      t[i] ≔  t[i] + t[i+1];
      i ≔  i - 1;
    }
}

You can we needed three loop invariants in the end, and I've commented what they are doing.

user_7645760
Related