问题标签 [spark-ada]

我在 SPARK 包中有一个过程，它从非 SPARK 包中调用一些函数。

GNAT 为我info: implicit function contract not available for proof (<function_name> may not return)从全局受保护类型调用函数的所有四个声明行提供了。

受保护类型函数在非 SPARK 包中定义如下，并使用Sim_Out在受保护类型私有部分中声明的记录。所有记录值都用 初始化0.0。

有什么替代方案可以解决这个问题？我确实已经添加了一些编译指示来为证明者提供额外的信息subtype Float_Signed1000 is Float range -1_000.0 .. 1_000.0，但这并没有像我预期的那样奏效。

我想在这里就这个话题提出你的建议。

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

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

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

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

我有一个功能，通过应用一个简单的检查信号是否在给定的容差范围内来监控受控信号。该函数被调用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编程知之甚少。

我可以理解这段代码中前置条件的含义和目的，但我在理解后置条件的含义和目的方面存在问题。在Push我知道这部分在推整数后增加指针（指针=指针~+1）。在Pop我理解这部分是在弹出整数后减少指针（Pointer=Pointer~ - 1）。

我正在尝试在此过程中添加派生子句，这是我的解决方案：

--# 从 Key 中导出 Index，从 Data 中导出 Data & I 从 Data 中导出；

我不确定，我需要帮助

我想证明这个过程中的循环将使用变体（绑定函数）终止

每次重复时，变量将是I并且下限是0 （I：= 0）
，大小I将减小直到达到下限0 我如何证明I在这个循环中会减小？

规格：

我想用 Assert 和 loop_invariants 编写 PolyPack 包的主体，以便 gnatprove 程序可以证明我的函数 RuleHorner 的正确性。

我写了我的函数 Horner 但我不知道如何在这个程序中放置断言和 loop_invariants 来证明它的正确性：

gnatprove：

溢出检查用于行 Y := (Y*X) + A(A'Last - I);

有人可以帮助我如何使用 loop_invariants 删除溢出检查

I want to find the smallest factor of a value with below specification

I wrote the body of the procedure try to cover all assert but always one of post condictions fail...

What i am doing wrong? Can someone help me past through all assert from specification?

1. 我有一个函数应该返回找到的岛屿的数量。

2. 我将这个函数命名为 Count_Islands，它接收一个 Map 类型的 Map_Array 参数，其中 Map 是一个岛屿数组。

3. Islands 是一个枚举类型，包含一组 Land、Water。

4. 我在 .ads 中有函数规范，在 .adb 中有正文

5. 我现在面临的问题是如何证明我的函数 Count_Islands'Result 将小于 (X * Y)

6. 我试过：with post => Count_Islands'Result < X * Y -- 每当我跑证明我得到的一切：中等：后置条件可能失败无法证明 Count_Islands'Result < X * Y

.ads 中的功能：

.adb 中的函数：

例如，在 4 * 5 的矩阵中，即我的 X = 4 和 Y = 5：

我希望群岛（土地）的输出结果为 1，小于 4 * 5。但 GNATprove 无法证明我的初始代码来分析它，使用 Post => Count_Islands'Result < X * Y;

有没有更好的方法来证明这个算术？谢谢你的帮助。