问题标签 [spark-2014]

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

这是函数的主体：

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

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

所以如果我有：

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

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

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

说我有类似的东西：

这给了我错误：

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

我的类型类似于：

如何使用 Ada 或 SPARK 在代码中指定该格式？

我在想Static_Predicate，但字符串必须以 3 个正整数开头，后跟一个破折号，后跟另一组 3 个正整数的条件不能用Static_Predicate表达式来描述。

如何找到字符串中作为空格字符的第一个字符并返回其索引，并使用一个可以用作其中一部分的表达式Contract_Cases？

例如，如果字符串是：

那么表达式应该返回4。

我有以下程序：

如果我运行gnatprove，我会得到以下结果，指向+标志：

中：溢出检查可能会失败

这是否意味着F (I - 1)可能等于Integer'Last，并且添加任何内容都会溢出？如果是这样，那么从程序的流程中是否不清楚这是不可能的？还是我需要在合同中指定这一点？如果不是，那是什么意思？

一个反例表明，gnatprove在这种情况下，确实担心 的边缘Integer：

medium：溢出检查可能会失败（例如 whenF = (1 => -1, others => -2147483648)和I = 2）

我试图证明“前置”的前提条件在执行下面的程序期间成立。前提是：

我在下面的代码中以 pragma 的形式尝试证明这一点。我可以证明这个前提条件适用于单循环，但不适用于双循环。尽管我找到了非常复杂的循环不变量的示例，但我找不到任何双循环示例。

规格：

身体：

错误是“循环不变量可能在第一次迭代中失败，无法证明 Illumination_Sources_Pkg.Length(Illumination_Sources) <= X*Y” 它并没有说它可能在第一次迭代后失败，所以这就是问题。

我正在使用 SPARK Discovery 2017 中 spark_io 示例中的 SPARK.Text_IO。

我的问题是，许多 SPARK.Text_IO 过程都有一个前提条件，即我不知道如何开始尝试证明标准输入是可读的并且我们不在文件末尾。如下面的代码所示，我的尝试是将 SPARK.Text_IO 过程（在本例中为 Get_Immediate）的前提条件添加到调用过程的前提条件中，认为这可能会向证明者保证该前提条件为真. 它没有用。这是我正在谈论的一个例子：

测试规格：

测试机构：

证明者给出的错误在 Get_Immediate 行“medium: precondition may fail” Get_Immediate 过程的原型和合同如下：

你如何向 SPARK 证明 Standard_Input 是可读的并且它不是文件结尾？

我有一个功能，通过应用一个简单的检查信号是否在给定的容差范围内来监控受控信号。该函数被调用is_within_limits。我有第二个函数is_within_expanded_limits，它的作用相同，但事先将扩展因子（扩大公差带）应用于配置的限制。monitor.config通过目标值和与该值的最大偏差或下限和上限阈值来配置限制。枚举monitor.config.monitoring_mode指定如何指定有效范围。

先看一下代码。

规格

执行

我的问题是断言pragma Assert (expanded_lower_threshold < expanded_upper_threshold)被标记为可能失败，我不明白为什么。我添加了该断言以检查我的代码是否没有像反转下阈值和上限阈值的关系那样奇怪，但主要是为了尝试断言。先决条件monitor.config.lower_threshold < monitor.config.upper_threshold与计算代码的结合expanded_lower_threshold应expanded_upper_threshold保证断言始终成立。问题出在哪里，我该如何解决？

我正在研究框架 Frama-c，我想知道 C/Frama-c 和 Spark Ada 之间是否存在等价关系。我知道比较这些不同的语言似乎很奇怪，但是在阅读了David A. Wheeler 的文章、Johannes Kanig 的比较和一些 SPARK 的用户手册之后，我很难猜测 SPARK 和 C/Frama-c/ACSL 是否给出相同的证明稳健性和相同的代码可靠性。

非常感谢您提前提供您的观点/经验！

PS：我对frama-c很陌生，对SPARK编程知之甚少。