
Sir,
I am trying to verify Quicksort. How do I notify Dafny that the max value of the input array to quicksort should be same as the max value of the output array of quicksort. I have tried this,
ensures forall i :: beg <= i <= end && (forall j :: beg <= j <= end && old (inArr[i]) >= old (inArr[j])) ==> old (inArr[i]) == inArr[Max(inArr, beg, end)];
ensures forall i :: beg <= i <= end && (forall j :: beg <= j <= end && old (inArr[i]) <= old (inArr[j])) ==> old (inArr[i]) == inArr[Min(inArr, beg, end)];
But this fails to do the job. As you can see, lines 244 and 245 are giving assertion violation here
http://rise4fun.com/Dafny/fWo1J



Basically, I just want to know how to refer to the max of the old values of an array (old as in the values that were there in it before the array was passed to quicksort)?



Sometimes I find it easier to to turn the array into a sequence
lemma nonEmptyArrayHasMax(arr: array<int>) returns (m:int)
requires arr != null;
requires arr.Length > 0;
ensures m == max(arr[..]);
{
m := max(arr[..]);
}
lemma nonEmptyArrayIntervalHasMax(arr: array<int>, beg: int, end: int) returns (m:int)
requires arr != null;
requires arr.Length >= end > beg >= 0;
ensures m == max(arr[beg..end]);
{
m := max(arr[beg..end]);
}
function max(s:seq<int>) : int
requires s > 0;
ensures forall a :: a in s ==> a <= max(s);
ensures max(s) in s;
{
if s == 1 then s[0]
else var maxtail := max(s[1..]);
if maxtail > s[0] then maxtail else s[0]
}



I see. Using array as a sequence, to say that max remains constant on quicksorting an array, is this valid : max (old (inArr[beg..end])) == max (inArr [beg..end]) ?

