SPARK 2014中幻影函数的编译

我希望将前后条件中的一些常见模式抽象为函数，以便使条件更具可读性。从文档看来，鬼功能解决了这个问题。SPARK 2014中幻影函数的编译

我依赖于断言中的溢出被消除（通过配置编译指示）的事实，所以我不相信我可以在代码中使用ghost函数。火花文档包含无码鬼功能的http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html#ghost-functions下面的例子：

function A_Nonexecutable_Ghost_Function (Lo, Hi : Natural) return Natural 
with Pre  => Lo <= Hi, 
    Post  => A_Nonexecutable_Ghost_Function'Result in Lo .. Hi, 
    Convention => Ghost, 
    Import; 
-- The body of the function is not declared elsewhere.

然而，这和任何其他影函数喜欢它，我尝试写，结果：

warning: null global effect assumed on imported subprogram

而且该警告停止编译。试图说Global =>()不起作用。我可以压制警告吗？ gnatprove命令行上没有明显的-Werror，我可以看到它们都被删除。

来源

2014-09-02 agl

正确的语法是Global => null而不是Global =>()，然后警告消失。

来源

2014-09-03 09:18:12 ksson

@manuBriot，我想过，一旦用户说'导入'，他们不应该不得不声明'全局=> null'？（在OP手册中没有提到这一点） – 2014-09-03 16:05:46

@SimonWright导入和全局是正交的方面。 Import表示Ada没有提供该子程序的主体。全局描述对子程序全局变量的影响。导入的子程序当然可以对全局变量产生影响，即使在SPARK中，Ghost函数也可以读取全局状态。所以鼓励用户指定两个方面是有道理的。 – ksson 2014-09-04 09:31:35

请再次参阅OP的手册链接。鬼函数中的'Import'是一个特殊的约定，意味着它是一个**不可执行的**函数，它根本就没有任何主体;如果它无法执行，它不会影响全局或任何其他状态。如果编译成功需要'Global => null'，如OP所述，那么手册是错误的。 – 2014-09-04 22:03:23

SPARK 2014中幻影函数的编译

回答

相关问题