ada - 没有可用于程序/功能的全局契约(Contract)

Question

我在调用标准 Ada-Text_IO.Put_Line 的 SPARK 模块中有一个过程。

在证明过程中，我收到以下警告 warning: no Global contract available for "Put_Line"。

我已经知道如何将相应的数据依赖契约添加到我自己编写的过程和函数中，但是如何将它们添加到我无法编辑源文件的其他人编写的过程/函数中？

我查看了 Adacore SPARK 2014 用户指南的第 5.2 节和第 7.4 节，但没有找到解决我的问题的示例。

Answer 1

这意味着分析器无法“看到”调用此函数时全局变量是否会受到影响。因此它假设这个调用没有修改任何东西(否则所有其他证据都可以立即被反驳)。对于您的特定示例，这可能是一个有效的假设，但在嵌入式系统上可能无效，在嵌入式系统中，Put_Line 的自定义实现可能会执行任何操作。

传递缺失信息的方式有两种:

1. 验证者可以检查函数的源代码。然后它可以尝试自己生成全局合约。
2. 明确指定全局契约(Contract)，参见 RM 6.1.4 ( http://docs.adacore.com/spark2014-docs/html/lrm/subprograms.html#global-aspects )

在这种情况下，您调用的过程是运行时系统 (RTS) 的一部分，因此源是不可见的，您可能不能/不应该更改它。

实践中要做什么？

抑制警告几乎从来都不是一个好主意，尤其是当您正在处理对安全至关重要的事情时。通常必须更改代码，直到警告消失，或者必须开始一些理由处理。

如果你对分析结果很在意，我建议不要使用这样的子程序。如果你真的需要在那里输出，要么编写你自己的过程来替换 RTS 子程序，要么确保子程序真的没有副作用。 Frédéric 所链接的内容进一步支持了这一点:即使被调用方没有副作用，您也不知道它是否会针对特定输入(例如，非常长的字符串)引发异常。

如果您对结果不是那么认真，那么您可以将这个特定的结果视为您可以接受的警告。