How to say that max of input array to Quicksort equals max of the output array of quicksort

May 7, 2014 at 12:52 AM
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
May 7, 2014 at 2:09 PM
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)?
May 8, 2014 at 9:37 AM
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]
}
May 8, 2014 at 5:16 PM
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]) ?