[Spark2014-discuss] Loop invariant for bubble sort

Claude Marche Claude.Marche at inria.fr
Thu Jul 3 08:57:48 CEST 2014


Hi,

Here is a Why3 version of bubble sort, fully proved with alt-ergo with a
time limit of 5 seconds.

Notice that since the inner loop modifies the array, the inner loop
invariant needed somehow to repeat the invariants of the outer loop.
This is part of the difficulty of bubble sort I would say.

Hope it will help you to design a Spark version of it. Keep us inform of
your achievements !

- Claude

On 07/02/2014 11:33 PM, Yannick Moy wrote:
> -- Hugues Jérôme (2014-07-02)
>>
>> Hi,
>>
>> I’m trying to prove a bubble sort, and face some issues on invariants (an area where I need some more insights than I expected). I took for granted from Claire on her last blog post that proving a sort being correct was “easy", and tried, but failed :(
> 
> Hi Jérôme,
> 
> The blog post says that proving sorting is "easier" than proving that the result is a permutation of the input, but not that it's "easy". So don't feel bad! :)
> 
>> Let me explain where I’m stuck (complete code is there: https://github.com/yoogx/spark_examples/tree/master/sparkle )
>> The problem is not the implementation of the sort itself, it may eventually be wrong (yet worked on a few tests, so I’m somewhat confident). My problem is on the analysis of the error messages and their interpretation towards a correct loop invariant 
>>
>> Here is where it starts;
>>
>> for I in reverse A'First + 1 .. A'Last loop
>> [..]      
>>       pragma Assert (A (I - 1) <= A (I));
>>       pragma Loop_Invariant
>>         (A (I - 1) <= A (I) and then -- proved
>>            (for all K in I .. A'Last => A (K - 1) <= A (K)));
>>
>> GNATProve accepts to discharge the assert, and the first part of the loop invariant.
>> It refuses to discharge the second part, and returns
>>
>> spark-bubble_sort.adb:46:44: warning: loop invariant might fail after first iteration, requires A (K - 1) <= A (K)
>>
>> OK, but if the first part of the invariant is proved, shouldn’t the tool infer the second part? This bugs me
> 
> No, this is not sufficient. The assertion 
>     pragma Assert (A (I - 1) <= A (I));
> simply restates what the tool knows from the loop invariant of the inner loop: the new value that has been put in A(I) is greater than previous values (and in particular A(I-1)).
> 
> But what you need to prove is that:
> 1) assuming only the loop invariant (so here: the array is sorted in increasing order from I-1 to A'Last)
> 2) ignoring everything else about variables modified in the loop (so here: we don't know anything about values of A between A'First and I-2)
> 3) executing the end of the loop (just the exit here), the test of the loop, continuing in those cases it does not exit, and the start of the loop (just the inner loop here), show that the loop invariant still holds
> 
> You can see that step (2) above does not allow proving the loop invariant in step (3). If you assume any value can be in the first part of the array A, then there is no way you can show that such a value when copied to index I is less than the value at index I+1.
> 
> Also, you need to know that the inner loop does not modify elements of the array after index I.
> 
> I attach a patch on Sort that allows to prove it completely in a few minutes, with a timeout of 120s and the proof strategy "progressively split", so using:
> 
> $ gnatprove -Pspark.gpr --timeout=120 --proof=progressive --limit-subp=spark-bubble_sort.ads:17
> 
> Note that I commented out the early exit when Finished is True. If you want to uncomment it and still prove the postcondition of Sort, you'll need to add new a loop invariant for the inner loop, that state that Finished remains True while the start of the array is sorted.
> 
>> GNATProve reports that because of the “guilty statement”, he has a counter example. But then why is the assert before discharged, as well as the first part of the invariant? 
> 
> Currently, GNATprove does not report counter-examples (although we're working on that), only traces that correspond to the path on which a check is not proved. But if you give too small a timeout, you'll still get these traces for the first path through the subprogram on which the prover does not answer "yes" in the given time! (provided you use the "proof by path" or "progressively split" proof strategy)
> 
> See for example the snapshot attached produced with SPARK GPL 2014 on the provable code, but this time using a short timeout of 1s.
> 
>> On a side note: with GPL 2014 toolset, the output in GPS is strange, I have a “magnify” icon on a line whose content is a duplicate of the line below, in place of the actual error message from GNATProve for line 46. Just try to prove the file with the per path strategy
> 
> I don't see this, look at the snapshot attached. Can you send a snapshot or a reproducer?
> 
>> Thanks for bringing some lights, I’m quite lost for now
> 
> As I said during the SPARK 2014 tutorial at Ada Europe last week, loop invariants are the heart of darkness of deductive methods! But there is nothing magic, once you understand how they work.
> 
> Hope that helps.
> --
> Yannick Moy, Senior Software Engineer, AdaCore
> 
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Project spark2014 discuss mailing list
> discuss at spark2014.forge.open-do.org
> https://lists.forge.open-do.org/cgi-bin/mailman/listinfo/spark2014-discuss
> 
-------------- next part --------------

(* {1 Bubble sort} *)

module BubbleSort

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArraySwap
  use import array.ArrayPermut
  use import array.ArrayEq


  let bubble_sort (a: array int)
    ensures { permut_all (old a) a } 
    ensures { sorted a }
  = 'Init:
    for i = length a - 1 downto 1 do
      invariant { permut_all (at a 'Init) a }
      invariant { sorted_sub a i (length a) }
      invariant { forall k1 k2: int. 
        0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] 
      }
      for j = 0 to i - 1 do
        invariant { permut_all (at a 'Init) a }
        invariant { sorted_sub a i (length a) }
        invariant { forall k1 k2: int. 
          0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] 
        }
        invariant { forall k. 0 <= k <= j -> a[k] <= a[j] }
        if a[j] > a[j+1] then swap a j (j+1);
      done;
    done

  let test1 () =
    let a = make 3 0 in
    a[0] <- 7; a[1] <- 3; a[2] <- 1; 
    bubble_sort a;
    a

  let test2 () ensures { result.length = 8 } =
    let a = make 8 0 in
    a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
    a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
    bubble_sort a;
    a

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let a = test2 () in
    if a[0] <> -5 then raise BenchFailure;
    if a[1] <> 6 then raise BenchFailure;
    if a[2] <> 17 then raise BenchFailure;
    if a[3] <> 42 then raise BenchFailure;
    if a[4] <> 53 then raise BenchFailure;
    if a[5] <> 69 then raise BenchFailure;
    if a[6] <> 91 then raise BenchFailure;
    if a[7] <> 413 then raise BenchFailure;
    a

end


More information about the Spark2014-discuss mailing list