Dafny can't prove simple sum

[harchaoui]

// Assuming the code below, I wrote this version, but the dafny doesn't complain about it, but the version where I start with s:= s + k; then k:= k + 1; gives an error!!!

//So I prove it with pen and paper!
//This code is correct iff (1) (2) (3) holds
// 1. the Hoare triple {Q} s:=0;k:=0 {Pinv}: holds : which TRUE √; and
// 2. {Pinv ∧ k < n } k:= k + 1; s:= s + k; {Pinv} Also holds :
//This one doesn't hold; as at the end of the proof, it gives
// s + k + 1 = (∑i|0<= i < k + 1 :i) ∧ (0 <= k + 1 <= n)
// s = (∑i|0<= i < k :i) - 1 ∧ (0 <= k + 1 <= n)

// but start accumulating the value in s, s:= s + k; and then increment k, k:= k + 1;
// gives the right proof as follows
// s + k = (∑i|0<= i < k + 1 :i) ∧ (0 <= k + 1 <= n)
// s = (∑i|0<= i < k :i) ∧ (0 <= k + 1 <= n)
// which means that the Hoare triple holds

// 3. This one holds too
// Pinv ∧ ⌝(k<n) => R

// I DON'T KNOW how Dafny works from the inside as I start experimenting with it, but it looks strange.

Dafny doesn't complain about this code (this is an incorrect, i think )

function Sum(n:nat) :(s:nat)
{
  if n==0 then 0 else n*(n + 1)/2
  // if n == 0 then 0 else n + Sum(n-1)
}

method TestSum(n:nat) returns(s:nat)
  requires  n >= 0 // pre-condition
  ensures s == Sum(n) // post-condition
{
  // {Q: n>=0 }
  s:= 0;
  var k:= 0;
  // {Pinv : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n)}
  while k < n
    invariant s == Sum(k) &&  0 <= k <= n
  {
    //   {Pinv ∧ k<n : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n) }
    k:= k + 1;
    s:= s + k;
    print(s,k);
    // {Pinv : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n) }
  }
  //   {Pinv ∧ not(k<n) : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n) not(k<n) }
  //   {R: s = (∑i|0<= i < k : b(i))  ∧  (0 <= k <= n) }
}

But it complains about this code (This is the correct one i think)

function Sum(n:nat) :(s:nat)
{
  if n==0 then 0 else n*(n + 1)/2
  // if n == 0 then 0 else n + Sum(n-1)
}

method TestSum(n:nat) returns(s:nat)
  requires  n >= 0 // pre-condition
  ensures s == Sum(n) // post-condition
{
  // {Q: n>=0 }
  s:= 0;
  var k:= 0;
  // {Pinv : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n)}
  while k < n
    invariant s == Sum(k) &&  0 <= k <= n
  {
    //   {Pinv ∧ k<n : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n) }
    s:= s + k;
    k:= k + 1;
    print(s,k);
    // {Pinv : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n) }
  }
  //   {Pinv ∧ not(k<n) : s = (∑i|0<= i < k :i) ∧  (0 <= k <= n) not(k<n) }
  //   {R: s = (∑i|0<= i < k : b(i))  ∧  (0 <= k <= n) }
}

[keyboardDrummer]

Why do you think your first version is incorrect and your second is not? What do you think of the error messages Dafny gives? Do you agree or disagree with them and why?

Have you ran both programs, either in your mind or on your machine, with particular inputs (start with just n == 1), to see whether the outputs are correct?

[harchaoui]

• Using a proof by hand using the Hoare Triple (HT) and the weakest precondition (WP) it clear that the first is incorrect and the second is correct. (if you can sketch one you will see it clear, and also if you follow steps i mentioned above you can also deduce that the second one reflect this fact but the first does not )

The second one gives this error, despite it is correct by proofs ( HT and WP)

• Dafny gives errors as follow (with possible counterexamples)

counterexamples given by dafny:

At "{" (file:///sum_err.dfy:32):
    n:int = 2
    defass:bool = false
    s:int = 0

At "s:= 0;" (file:///sum_err.dfy:34):
    n:int = 2
    defass:bool = true
    s:int = 0

At "var k:= 0;" (file:///sum_err.dfy:35):
    n:int = 2
    defass:bool = true
    s:int = 0
    k:int = s

At "while k < n" (file:///sum_err.dfy:37):
    n:int = 2
    defass:bool = true
    s:int = 1
    k:int = s
    preLoop$loop:bool = defass

At "s:= s + k;" (file:///sum_err.dfy:41):
    n:int = 2
    defass:bool = true
    s:int = n
    k:int = 1
    preLoop$loop:bool = defass

At "k:= k + 1;" (file:///sum_err.dfy:42):
    n:int = 2
    defass:bool = true
    s:int = n
    k:int = n
    preLoop$loop:bool = defass

The Second shows No error despite, it is incorrect by proof

[Dargones]

The counterexample is correct as far as I can tell. In particular, it is showing you an iteration of the loop that begins with s==1 and k==1 (Sum(1) == 1, so the invariant is respected) and ends with s==2 and k==2, which violates the invariant because Sum(2) != 2. I am not certain how that translates to the proof sketch but the counterexample makes it clear that the correct sequence of statements begins with k:= k+1;

[harchaoui]

Can you tell me what is {Pinv ∧ k<n} s:= s+ k; k:=k+1; {Pinv} and {Pinv ∧ k<n} k:=k+1;s:= s + k {Pinv}?

something has to change if both are correct? either Hoare and all the language of the weakest precondition has to change or Dafny has to change something, i don't know what it is?