[Spark2014-discuss] Loop invariant for bubble sort

Hugues Jérôme hugues.jerome at gmail.com
Fri Jul 4 17:07:52 CEST 2014


Hi,

Le 4 juil. 2014 à 16:27, Claire Dross <dross at adacore.com> a écrit :

> I have completed the selection sort example to also prove that the resulting array is sorted. It still proves with CVC4 and alt-ergo with a timeout of 5 seconds.
> 
> Hope this helps,

Thanks, you relieve me of one exercise ;-)

Note that I pushed the bubble sort on github, I still need to add credits and lot of comments. 
I’ll then study your selection sort and comment invariants as another exercise

I’m curious about the ghost code: I understand it adds information in the execution flow that guides the prover.
Yet, from your code, there is no distinction between ghost code and “useful” code, except for a comment.
Hence, this code would also be used as part of the compilation process, and would ultimately slow down the process, for instance the call to Prove_Swap_Perm

shouldn’t you introduce a pragma, e.g. pragma SPARK_Ghost (<procedure_call>) so that the procedure is called in SPARK_Mode, but ignored otherwise, like pragma Assert ?

Regards,





More information about the Spark2014-discuss mailing list