[Spark2014-discuss] Loop invariant for bubble sort
dross at adacore.com
Thu Jul 3 10:09:13 CEST 2014
Le 03/07/2014 09:42, Yannick Moy a écrit :
> Until then, the user of SPARK has to either come up with such a local library, or "inline" these properties in the loop invariants he/she writes.
You could also use the external axiomatization mechanism to prove axioms
for your properties, like in the standard library of Why. I have done
that for the permutation example already, I will write a blog post about
it shortly. You can find the test in N120-055__perm in the testsuite.
Everything is proved by alt-ergo with a timeout of 5 seconds.
More information about the Spark2014-discuss