not for lean but for dafny, but hoare triple must hold ..

Stream: new members

[Abdel Ali 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.

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) }
}

[Henrik Böving]

The odds you are going to find Dafny help in a Lean Zulip are rather low I am afraid.

[Abdel Ali Harchaoui]

Maybe because I found this dafny and lean on the archive , https://leanprover-community.github.io/archive/stream/113489-new-members/topic/Lean.20vs.20Dafny.3A.20Why.20can%27t.20I.20just.20put.20a.20bunch.20of.20assertions.2E.2E.2E.html

[Abdel Ali Harchaoui]

But i think I will delete it and I'm sorry :pray:

[Notification Bot]

This topic was moved here from #general > not for lean but for dafny, but hoare triple must hold .. by Eric Wieser.