[Spark2014-discuss] Loop invariant for bubble sort

David MENTRÉ dmentre at linux-france.org
Wed Jul 2 21:24:22 CEST 2014

Hello Jérôme,

2014-07-02 18:32, Hugues Jérôme:
> 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

I looked at your code and found no obvious reason why your two loop 
invariants are not proved. For the inner loop, the "for all K in A'First 
.. J => (A (K) <= A (J + 1)" condition might be too strong for automated 
provers (no induction) but I'm not sure of it.

One proposal to make progress (but you might already have done it): 
compile your code with assertions compiled as dynamic check (-gnatE or 
-gnata or both, can't remember) and apply your tests on it. If those 
tests fail, you'll have a concrete counter-example to work on. If your 
tests work, then you logical assertions are probably correct but they 
should be reformulated so the prover can prove them.

Good luck!

More information about the Spark2014-discuss mailing list