[Spark2014-discuss] Loop invariant for bubble sort
dmentre at linux-france.org
Wed Jul 2 21:24:22 CEST 2014
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.
More information about the Spark2014-discuss