问题标签 [spark-ada]

我有两个函数：InefficientEuler1Sum 和 InefficientEuler1Sum2。我想证明它们都是等价的（给定相同输入的相同输出）。当我运行 SPARK -> Prove File（在 GNAT Studio 中）时，我pragma Loop_Invariant(Sum = InefficientEuler1Sum(I));在文件 euler1.adb 中收到有关行的此类消息：

1. loop invariant might fail in first iteration
2. loop invariant might not be preserved by an arbitrary iteration

似乎（例如，在尝试手动证明时）函数 InefficientEuler1Sum2 不知道 InefficientEuler1Sum 的结构。将这些信息提供给它的最佳方式是什么？

文件 euler1.ads：

文件 euler1.adb：

Spark 简介课程包含一个示例（#5），其中GNATprove 未能证明在交换数组的两个元素的过程中没有出现别名：

GNATprove 说p.adb:13:13: medium: formal parameters "X" and "Y" might be aliased (SPARK RM 6.4.2)。这似乎是一个有效的错误，因为传递给的索引Swap_Indexes可能相等。但是，在 中添加前提条件Pre => I /= J后Swap_Indexes，GNATprove 仍然无法证明缺少别名。为什么这个前提条件不充分？

所以我有以下声明：

它用于

这会产生编译错误： volatile object cannot act as actual in a call (SPARK RM 7.1.3(10))

现在，Clock使用的是 volatile 。但是我已经删除了对的调用Clock，我仍然得到相同的结果。

此外，我尝试将Object类型替换为类型，Integer并且我没有来自 Ada 编译器的任何投诉。有人可以解释一下吗，因为我看不出这是如何将易失性对象放入实际的任何地方。

刚刚尝试使用以下记录，我得到了相同的结果：

我已经尝试搜索文档和代码，但我无法找到这是什么以及如何更正它。

设想：

我正在使用 Ada SPARK 向量库，并且我有以下代码：

代码调用时出现错误：

指向Empty_Vector. 困难在于Empty_Vector定义似乎导致问题的原因Capacity。0现在我不确定如何处理Capacity似乎在类型定义中的问题（已经查看过a-cofove.ads）。

所以基本上我被困在如何解决这个问题上；或者相当如何发现未来发生的这种情况。

我的问题总结

我正在为我的 SHA256 函数使用libsparkcrypto 库。我发现我不能Assert这样x = y暗示Sha256(x) = Sha256(y)。任何帮助将不胜感激。

代码

测试包.adb

测试包.ads

输出

我收到的错误是：

testpackage.adb:8:25: medium: 断言可能失败，不能证明 LSC.SHA2.Hash_SHA256 (X) = LSC.SHA2.Hash_SHA256 (Y) [可能的解释：testpackage.ads:8 的子程序应该在前置条件][#0]

我的gnatprove.out：

我不是 SPARK 的用户。我只是想了解语言的功能。

例如，可以使用 SPARK 来证明 Quicksort 实际上对给它的数组进行排序吗？

（希望看到一个例子，假设这很简单）

我的目标是证明霍纳法则是正确的。为此，我将霍纳当前计算的值与“实数”多项式的值进行比较。
所以我做了这段代码：

这应该证明不变量。不幸的是， gnatprove 告诉我：

在这种情况下 Y=-1 是如何工作的？你有任何想法如何解决这个问题吗？

我试图证明我在 Ada 中的 Select Sort 实现是正确的。我尝试了一些循环不变量，但使用 gnatprove 只能证明内循环的不变量：

Gnatprove 告诉我 selection.adb:15:14: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove Sorted( A (A'First..I)) (e.g. when A = (-1 => 0, 0 => 0, others => 1) and A'First = -1) 你有什么想法可以解决这个问题吗？

我对 Ada 完全陌生，并且一直在尝试实现一些基础知识。我有一个简单的功能来掷硬币 - 不是随机的，应该将正面翻转为反面，反之亦然。我添加了一个后置条件，即翻转（硬币）！=硬币。应该说翻转的硬币不能等于原始硬币，但是当我尝试使用 --mode gold 证明文件时，我收到以下警告：

这是广告文件

这是 .adb 文件

任何帮助都会很棒！在接下来的两周里，我会问更多的问题。

我是一个 Ada 菜鸟，正在编写一个简单的函数，它采用整数列表并将每个元素递减 1。我的青铜模式证明通过了，但尝试在 main 中实际使用该函数以查看它是否真的在做它应该证明是一场斗争。我不确定如何初始化数组并分配值（应该是 0..10）。我也不确定我是否可以只用一个递减函数而不是递减（整数）和递减列表（ArrayOfNumbers）函数来实现这一点。或者，如果我做得对。任何帮助都是王牌，我没有找到任何好的文档，所以我觉得我应该猜测我的方式。这个包被称为flip_coin，因为它是早期任务的一部分，任何与翻转硬币有关的事情都可以忽略！

这是规范文件：

这是正文文件：

这是主文件：

这是我尝试运行时的错误：

任何帮助再次非常感谢。TIA