[Spark2014-discuss] Loop invariant for bubble sort

Yannick Moy moy at adacore.com
Fri Jul 4 17:16:52 CEST 2014


-- Hugues Jérôme (2014-07-04)
> 
> 
> 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

Correct. In the absence of ghost variables and procedures in current SPARK language and tools, she has simply marked the code as ghost in comments. But when ghost code is available, this code is eligible for being ghost code.

> 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 ?

Indeed, ghost code is on the roadmap to be included in SPARK 2014 language and tools for the next release.
Currently, you can only define ghost functions. In the next release, you should be able to define ghost variables and statements as well, and the compiler will remove ghost code when compiled with assertion policy Ghost set to Ignore. (so for example, by default you won't get it, and if you compile with -gnata you will get it)
--
Yannick Moy, Senior Software Engineer, AdaCore






More information about the Spark2014-discuss mailing list