[Spark2014-discuss] Loop invariant for bubble sort

Claire Dross 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 mailing list