[Spark2014-discuss] Loop invariant for bubble sort
hugues.jerome at gmail.com
Fri Jul 4 17:07:52 CEST 2014
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 ?
More information about the Spark2014-discuss