问题标签 [spark-ada]

我正在使用 SPARK 方法对 Ada 进行自动列车保护。这是我在 SPARK 中的规格：

这是我的艾达：

我想知道为什么在函数 Read_Sensor_Majority 中我不能使用 State(1) 或任何 State() 数组值。如果有使用它们的方法，我是否应该在 SPARK 的规范中添加任何内容来实现它？

它显示的错误是：

您好，我正在尝试从此函数编写证明注释..这是使用 Spark 编程语言编写的

这是 .ads 文件

这些是我使用 spark 检查器检查文件后遇到的错误

对于一个学校项目，我必须写一篇关于 SPARK 编程语言的论文，我确实这样做了，但其中一部分是编写一个短程序，它接受一个整数 n 并输出从 1 到 n 的平方和。在 C++ 中，程序看起来像这样：

我对 SPARK 一点也不熟悉，我在 Ada 中找到了一个类似的程序并稍微修改了它，所以它可以使用整数而不是双精度数并输出结果（55）。

现在的问题是如何将这个 Ada 程序变成一个 SPARK 程序。我尝试将 Ada.Text_IO 更改为 Spark_IO，但 IDE（GPS）给了我“找不到文件 spark_io.ads”。”此外，该程序应该使用任意整数 n，而不仅仅是 5，如示例中所示。任何帮助将不胜感激。

我对 Ada/SPARK 很陌生。我试图从这里学习一些教程——

http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html

假设我正在运行此处给出的 ISQRT 示例 ( http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#id19 )。所有代码（*.ads和*.adb）都捆绑为一个名为的项目isqrt.gpr，我正在运行的命令是——

:~$ gnatprove -gnato13 -P isqrt.gpr

我得到的输出是——

该教程说我需要提供一个调用证明者的开关-gnato13，以便它跳过一些溢出检查。但显然这个开关是不可接受的。

任何想法？

我不喜欢编码，但我真的很喜欢 Ada，而且我对它很陌生。那么你能向我澄清这些观点吗？

如果您的计算机具有单个非线程 CPU，则任务仍然是单 CPU。当然，这同样适用于 C 或 C++中的分叉。

问题：你认为在这种情况下，Ada 任务分配比分叉有什么好处吗？

我也想知道为什么 SPARK 禁止任务分配（我知道这是为了安全，但确切地说，禁止任务分配如何提高安全性。）

我的第三个也是最后一个问题，如果我想提供“安全任务”（在 Ada 中），我可以设想哪些任务限制才能使使用它们（任务）“安全”。

谢谢，

我想编写一个简单的函数，在给定的整数数组中找到最大的数字。这是规格：

这是函数的主体：

当我尝试用 SPARK 证明这个函数时，它说后置条件可能会失败。我现在试图理解这一点 5 个小时，但我不知道为什么会这样说。这真的很烦人，这个功能必须工作。你知道为什么 SPARK 的行为如此奇怪吗？该函数不满足其后置条件的数据示例是什么？它总是返回一个直接取自给定数组的值，并且它总是最大的。

如何为对数组元素求和的函数编写 Spark 后置条件？（Spark 2014，但如果有人告诉我如何为早期的 Spark 做这件事，我应该能够适应它。）

所以如果我有：

在我的特定情况下，我不需要担心溢出（我知道初始化时的总数是多少，它只能单调减少）。

大概我在实现中需要一个循环变体来帮助证明者，但这应该是后置条件的直接变体，所以我还不担心。

如何在 SPARK Ada 中实例化非库级包？

说我有类似的东西：

这给了我错误：

大概我需要为 Ada.Numerics.Discrete_Random 关闭 SPARK_Mode，但我无法找到放置 pragma 的正确位置。

我目前正在大学实时编程语言课程中学习 Ada，并且有一个关于 SPARK 的问题。

我正在从事一个项目，其任务是监控离网电源。这项任务对机器安全至关重要，因此应尽可能避免错误，例如用 SPARK 证明。

我收到了这个奇怪的错误，我无法找到解决方法11:14 tasking in SPARK requires sequential elaboration (SPARK RM 9(2)) violation of pragma SPARK_Mode

原始代码有点长，但我能够通过一个最小的示例得到相同的错误。

规格：

实施：

任何帮助表示赞赏:-)

我目前正在大学实时编程语言课程中学习 Ada，并且有一个关于 SPARK 的问题。

我正在从事一个项目，其任务是监控离网电源。这项任务对机器安全至关重要，因此应尽可能避免错误，例如用 SPARK 证明。我能够在 stackoverflow 上解决一些其他问题，但我仍然遇到无法通过用户指南中的快速搜索修复的错误。

错误是call to a volatile function in interfering context is not allowed in SPARK参考中的if monitoring_interface.is_all_config_set then ...行

该函数is_all_config_set在我用于任务间通信的受保护类型中定义。

相应的身体是

这里有什么问题？