问题标签 [spark-2014]

我用 SPARK 2018 解决不了这个问题，我想我需要一些不变量来解决溢出的问题，但是我已经尝试了一切，找不到。如果有人可以阐明我的问题。

我将通过简单模式和二进制模式通过连续平方来尝试求幂。

非常感谢您提前。

这是错误：

这是我的代码 .ads

这是我的代码.adb

需要 Ada 编程语言 spark 2014 的词汇和语法表，请有人帮忙。提前致谢。

Spark 的新手，Ada 的新手，所以这个问题可能过于宽泛。但是，作为理解 Spark 的尝试的一部分，它是真诚地询问的。除了直接回答以下问题外，我还欢迎对风格、工作流程等提出批评。

作为我第一次涉足 Spark，我选择尝试实现（简单）并证明正确性（迄今为止不成功）该功能。

问题：实现和证明此功能正确性的正确方法是什么？

我从以下开始util.ads：

我没有先决条件，因为输入的范围完全表达了唯一有趣的先决条件。我根据数学定义写的后置条件；但是，我在这里有一个直接的担忧。如果X是Positive'Last，则2**(Floor_Log2'Result + 1)超过Positive'Last和Natural'Last。我已经在这里反对我对 Ada 的有限知识，所以：子问题 1：后置条件中子表达式的类型是什么，这是溢出问题吗？有没有通用的方法来解决它？为了避免这种特殊情况下的问题，我将规范修改为不太直观但等效的：

有很多方法可以实现这个功能，我现在并不特别关心性能，所以我对其中任何一种都很满意。我认为“自然”实现（鉴于我特定的 C 背景）类似于以下内容util.adb：

正如预期的那样，尝试在没有循环不变量的情况下证明这一点会失败。结果（此结果和所有结果均为 GNATprove 级别 4，从 GPS 调用为gnatprove -P%PP -j0 %X --ide-progress-bar -u %fp --level=4 --report=all）：

这里的大多数错误对我来说都是基本的。从第一次溢出检查开始，GNATprove 无法证明循环在少于Natural'Last迭代次数（或根本没有？）内终止，因此它无法证明I := I + 1没有溢出。我们知道情况并非如此，因为Remaining正在减少。我试图通过添加循环变体来表达这一点pragma Loop_Variant (Decreases => Remaining)，并且 GNATprove 能够证明循环变体，但潜在的溢出I := I + 1没有改变，推测是因为证明循环完全终止并不等于证明它在少于Positive'Last迭代中终止。更严格的约束将表明循环最多在Positive'Size迭代中终止，但我不确定如何证明这一点。相反，我通过添加一个“强迫它”pragma Assume (I <= Remaining'Size); 我知道这是不好的做法，这里的目的纯粹是为了让我看看我能在第一期“被掩盖”的情况下走多远。正如预期的那样，这个假设让证明者可以证明实现文件中的所有范围检查。子问题2：证明I在这个循环中不溢出的正确方法是什么？

但是，我们在证明后置条件方面仍然没有取得任何进展。显然需要循环不变量。保持在循环顶部的一个循环不变量是pragma Loop_Invariant (Remaining * 2**I <= X and then X/2 < Remaining * 2**I); 除了为真之外，该不变量还有一个很好的特性，即当循环终止条件为真时，它显然等同于后置条件。然而，正如预期的那样，GNATprove 无法证明这个不变量：medium: loop invariant might fail after first iteration, cannot prove Remaining * 2**I <= X[#20]. 这是有道理的，因为这里的归纳步骤是不明显的。通过对实数进行除法，可以想象一个简单的引理说明for all I, X * 2**I = (X/2) * 2**(I+1)，但是（a）我不希望 GNATprove 在没有提供引理的情况下知道这一点，并且（b）整数除法更加混乱。那么，子问题 3a：这是尝试用来证明此实现的适当循环不变量吗？子问题 3b：如果是这样，证明它的正确方法是什么？从外部证明一个引理并使用它？如果是这样，那究竟是什么意思？

在这一点上，我想我会探索一个完全不同的实现，只是看看它是否会导致不同的地方：

这对我来说是一个不太直观的实现。我没有过多地探索第二个实现，但我把它留在这里展示我尝试了什么；为主要问题的其他解决方案提供潜在途径；并提出额外的子问题。

这里的想法是通过明确终止和范围来绕过 I 和终止条件溢出的一些证明。令我惊讶的是，证明者首先在溢出检查表达式时窒息2**I。我曾期望2**(X'Size - 1)可以证明在范围内X——但我又一次遇到了我的 Ada 知识的限制。子问题 4：这个表达式在 Ada 中实际上是无溢出的吗？如何证明？

事实证明这是一个很长的问题......但我认为我提出的问题，在一个几乎微不足道的例子的背景下，是相对普遍的，并且可能对像我一样试图尝试的其他人有用了解 Spark 是否以及如何与他们相关。

规格：

我想用 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?

代码如下所示：

规格：

身体：

正文中没有证明错误，错误仅在规范上：

后置条件可能失败，无法证明 Record_Field_X(Record) = Record_Field_X(Record'Old)

规范和程序结束时的 Assert_And_Cut 之间的“其他后置条件”相同。

请注意使用更简单字段的检查，例如 X_Count：

Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)

不要让 gnatprove 抱怨。

过程中的证明者有很多工作，所以通常，当证明后置条件出现问题时，它有助于在过程结束时断言该条件以“提醒”证明者这是重要的事实。通常，这是可行的，但在一种情况下，由于某种原因它不起作用。

我在这里有什么选择？

这可能是什么原因？

也许我应该只增加运行证明程序的机器上的 RAM，这样它就不会丢失Record_Field_X(Record) = Record_Field_X(Record_Old)程序结束与其后置条件之间的事实？（我目前正在一台具有 32GB 内存的机器上执行此操作，该内存专门用于运行 gnatprove，使用--memlimit=32000 --prover=cvc4,altergo --steps=0）

也许有一些我不知道的技术？

也许我唯一的选择是手动证明？

我正在使用 spark 社区 2019 版。

我的问题总结

我正在为我的 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 实际上对给它的数组进行排序吗？

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

我正在将我在 Dafny 中进行的一项练习翻译成 SPARK，其中可以根据递归函数验证尾递归函数。Dafny 来源（已审查，因为它可能仍用于课程）：

到目前为止，我在 SPARK 中得到了什么：

我似乎无法弄清楚如何表达这种decreases n情况（现在我想起来可能有点奇怪......但几年前我已经为它评分了，所以我该判断谁，问题仍然是如何把它做完）。结果，我收到可能溢出和/或无限递归的警告。

我猜要添加一个前置或后置条件。试过Pre => n <= 1显然不会溢出，但我仍然收到警告。除此之外Post => Sum'Result <= n**n，警告会消失，但该条件会得到“后置条件可能失败”的警告，这是不对的，但猜测证明者无法判断。也不是我应该检查的表达式，但我似乎无法弄清楚Post我在寻找什么。可能是非常接近递归表达式的东西，但我的尝试都没有奏效。一定错过了一些语言结构......

那么，我该如何表达递归约束呢？

编辑1：

按照此 SO 答案和此 SPARK 文档部分的链接，我尝试了以下操作：

但是从 SPARK 收到这些警告：

继续我从 Dafny 转录到 SPARK 的努力，我遇到了为数组创建先决条件的问题，该数组应该在调用函数时进行排序：

我错过了什么？