2

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

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

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

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

4

3 回答 3

3

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

有两种方法可以传达缺失的信息：

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

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

在实践中该怎么做？

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

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

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

于 2018-01-24T20:57:13.277 回答
2

可在此处找到用于开发 SPARK 应用程序的包装器包： https ://github.com/joakim-strandberg/aida_2012

于 2018-02-02T09:31:26.383 回答
1

我认为你不能在你不拥有的代码上添加 Spark 合约，尤其是来自 Ada 标准的代码。

关于Text_Io，我在参考手册中发现了一些可能对您有价值的内容。

编辑

根据“使用 Spark 构建高完整性应用程序”一书，与Martin 所说的相比，另一个解决方案是创建一个包装器包。

由于 Spark 要求您处理 Spark 包，但允许您依赖带有 Ada 主体的 Spark 规范，因此解决方案是构建一个包装您的 Ada.Text_io 调用的 Spark 包。

这可能很乏味，因为您必须包装可能的异常，可能定义特定类型等等，但是这样，您就可以在完整的 Spark 包上释放 VC。

于 2018-01-24T08:23:40.467 回答