
The following bubble sort algorithm
http://rise4fun.com/Dafny/p3l
can be verified if all the postconditions and invariants about the permutation property are of the form perm(a[..],old(a[..])). However, for didactic purposes I have tried to do the experiment of asserting about the exact part of the array that has been permuted.
I have surprinsingly discover two issues:
1. You should add
assert a[..a.Length] == a[..];
assert old(a[..a.Length]) == old(a[..]);
to help Dafny in the inference of the post.
For that, change assert by assume in the innerloop assertion.
2. The innerloop assertion is violated, in spite that is a postcondition of the method step.


Nov 21, 2015 at 10:46 AM
Edited Nov 21, 2015 at 1:08 PM

I think it is to do with a missing lemma about perm. Something like:
lemma trans(a:seq<int>,a':seq<int>,a'':seq<int>, i:int)
requires 0 <= i < a;
requires a == a' == a'';
requires perm(a[..i],a'[..i]);
requires a[i..]==a'[i..];
requires perm(a'[..i+1],a''[..i+1]);
requires a'[i+1..]==a''[i+1..];
ensures perm(a[..i+1],a''[..i+1]);
With this lemma it would prove like this:
method bubbleSort (a: array<int>)
requires a != null
requires a.Length >= 2
modifies a
ensures perm(a[..],old(a[..]))
ensures sorted(a)
{
ghost var a' := a[..];
var i := 1;
while i < a.Length
modifies a
invariant 1 <= i <= a.Length;
invariant sortedBetween(a,0,i);
invariant perm(a'[..i],a[..i]);
invariant a'[i..]==a[i..];
{
ghost var a'' := a[..];
step(a,i);
assert perm(a[..i+1],a''[..i+1]);
trans(a',a'',a[..],i);
i:= i+1;
}
assert a[..a.Length] == a[..];
assert old(a[..a.Length]) == old(a[..]);
}
http://rise4fun.com/Dafny/0c2



Here is a version which verifies
http://rise4fun.com/Dafny/ZNO7
lemma trans(a:seq<int>,a':seq<int>,a'':seq<int>, i:int)
requires 0 <= i < a;
requires a == a' == a'';
requires perm(a[..i],a'[..i]);
requires a[i..]==a'[i..];
requires perm(a'[..i+1],a''[..i+1]);
requires a'[i+1..]==a''[i+1..];
ensures perm(a[..i+1],a''[..i+1]);
{
assert a[i] == a'[i];
assert multiset(a[..i]) == multiset(a'[..i]);
assert multiset(a'[..i+1]) == multiset(a''[..i+1]);
assert multiset(a[..i])+multiset{a[i]} == multiset(a'[..i])+multiset{a'[i]};
MultiSetSequenceDist(a,i);
MultiSetSequenceDist(a',i);
assert multiset(a[..i+1]) == multiset(a'[..i+1]);
assert multiset(a'[..i])+multiset{a'[i]} == multiset(a'[..i+1]) == multiset(a''[..i+1]);
assert multiset(a[..i+1])==multiset(a''[..i+1]);
}
lemma MultiSetSequenceDist(a:seq<int>,i:int)
requires 0 <= i < a;
requires a != [];
ensures multiset(a[..i])+multiset{a[i]} == multiset(a[..i+1])
{
MultiSetSequenceDist'(a[..i],a[i]);
assert multiset(a[..i])+multiset{a[i]} == multiset(a[..i]+[a[i]]);
assert a[..i]+[a[i]] == a[..i+1];
}
lemma MultiSetSequenceDist'(a:seq<int>,i:int)
ensures multiset(a)+multiset{i} == multiset(a+[i])
{ }


Nov 23, 2015 at 8:51 AM
Edited Nov 23, 2015 at 8:52 AM

A million of thanks for your verified version, but let me insists that I would like to figure out what is the cause of the issue related in the second fact of my question: Why Dafny is not able to prove the assertion perm(a[..i+1],old(a[..i+1])); after
the method call step(a,i)? Note that it is in the ensures of the method contract. Not so importantly, I also found odd that properties a[..a.Length] == a[..]; old(a[..a.Length]) == old(a[..]); should be asserted as help for Dafny. Best, Paqui



1) I think that the meaning of "old" is different in the post condition of the method and the body of the loop after the call. In both cases it is referring to the heap at the start of method execution, however in the loop it is referring
to the currently executing method, whereas in the postcondition it is referring to the called method. This is one reason why I gave the earlier states of the array explicit names in my version.
2) In my experience there are a lot of things Dafny doesn't immediately know about sequences. I presume (but don't know) that this is a performance design issue. Presumably one could add more (or different) axioms about sequences to the Dafny prelude,
which would enable Dafny to deal with cases like yours, but I expect the cost would be decreased verification performance as the solver considers more possible proofs involving those axioms. I suppose a way to check would be to add the relevant axiom and then
rerun the Dafny test cases to look for any changes in execution time.



Thank you for your support , doing so cleared things up quite a lot. Paqui

