问题标签 [formal-verification]

为了学习依赖类型，我正在用 Idris 重写我的旧 Haskell 游戏。目前游戏“引擎”使用内置的整数类型，例如Word8. 我想证明一些涉及这些数字的数值属性的引理（例如，双重否定是身份）。但是，不可能对原始算术运算的行为说些什么。什么会更好，只使用believe_me或其他手动操作（至少对于最基本的属性），或者使用 和其他“高级”数字类型重写我的Nat代码Fin？

我正在尝试编写以下函数：

我不知道怎么写这个。对我来说，这是不言自明的直觉，但编译器不接受 refl 作为它的证明。

我经常不得不证明这些事情，例如，证明如果两个非空列表相等，那么它们的头是相等的。

对此的一般方法是什么？这是否与 Conor McBride 的在构造函数的返回中具有函数的“green-goo”有关？

我试图在 C 中证明类似 strlen 的函数，但 frama-c 不证明后置条件和loop variant len子句。我不明白为什么！

我试过的：

我究竟做错了什么？

纯 函数是类似于数学函数的函数，其中没有与“现实世界”的交互，也没有副作用。从更实际的角度来看，这意味着纯函数不能：

• 打印或以其他方式显示消息
• 随意
• 取决于系统时间
• 更改全局变量
• 和别的

所有这些限制使得对纯函数的推理比对非纯函数的推理更容易。大多数函数应该是纯函数，这样程序可以减少错误。

在像 Haskell 这样具有庞大类型系统的语言中，读者可以从一开始就知道函数是纯函数还是非纯函数，从而使后续阅读变得更容易。

在 Python 中，这个信息可以通过@pure放在函数顶部的装饰器来模拟。我也希望那个装饰器能够真正做一些验证工作。我的问题在于这样一个装饰器的实现。

现在，我只是在函数的源代码中查找流行语，例如globalor randomor print，如果找到其中一个，我会抱怨。

然而，这感觉就像一个奇怪的黑客，可能会也可能不会取决于你的运气，你能帮我写一个更好的装饰器吗？

我想形式化一些知识并在可能被称为完全声明性的Horn 逻辑（或完全声明性的 Prolog）中执行查询。谁能提供一些有关如何实施它的指导方针？我简要回顾了上面链接中的详细描述：

形式语言是 Prolog 的（核心）语言：“程序”是 Prolog 中的一组规则和事实（包括函数和变量，基本上只包含用户定义的谓词）。

然而，与 Prolog 相比，我正在寻找一种相对于逻辑程序的标准声明语义而言是健全和完整的实现——最小的 Herbrand 模型（即，归纳定义的一组基本术语）。在逻辑编程的理论工作中，这通常是研究的对象，众所周知，可以（在“递归可枚举”意义上）获得对查询的健全和完整的答案，例如，使用 SLD 解析受以下条件：

• 匹配规则的公平搜索（例如，Prolog 的深度优先搜索不公平）；
• 与“发生检查”的统一（检查变量没有出现在与之统一的术语中）。

我正在寻找一种基于现有功能的简洁实现，而不是发明轮子。我看到的两个更有希望的方向是将其实现为 Prolog 的元解释器，或者作为某些定理证明器的一部分。任何具有这些领域实践知识的人都可以就如何实施它提供一些指导吗？能否在miniKanren中轻松实现？

我的意图是以完全声明的方式形式化一些知识。这种形式化的关键特征是它精确地对应于（单调）归纳的数学概念，因此可以很容易地用归纳论证来推理知识及其属性。

假设我们有一个列表：

请注意，我说的是可修改列表！还有一个简单的递归长度函数：

自然，它仅在列表非循环时终止：

请注意，这个谓词被实现为递归函数，也不会在循环列表上终止。

通常我会看到使用列表长度作为有界递减因子的列表遍历终止证明。他们认为这Length是非负的。但是，在我看来，这个事实 ( Length l >= 0) 首先是从 of 的终止而来的Length。

你如何证明，在（或等效的，更好定义的谓词）列表Length上终止并且是非负的？NonCircular

我在这里错过了一个重要的概念吗？

在以下函数定义（list.c）中：

frama-c 失败并显示以下消息：

该示例直接取自ACSL 手册。为什么它l与函数的唯一参数相关联时遇到麻烦？

PS我使用frama-c版本：Sodium-20150201

是否可以对 ACSL 中定义的归纳谓词使用归纳？

考虑ACSL 手册中的以下示例：

我试图证明以下引理：

Alt-Ergo 在这里失败了，所以我求助于手动 Coq 推理：

但是当 I 时Search P_reachable，我发现只生成了两个公理：

并且没有感应原理。所以我不能申请induction P_reachable或destruct P_reachable。

我使用frama-c版本 Sodium-20150201 的 WP 插件。

要重现，您可以运行frama-c -wp -wp-rte -wp-prover coqide file.c，其中file.c包含List和reachable定义和next_null_reachable引理。

\freeable鉴于它是前提条件，我如何证明指针是？

WP还没有完全支持分配是否是结果？

如果不支持，为什么 WP 会生成typed_fint_call_free_deallocation_pre_freeable条件，我该如何丢弃它？

PS我使用钠frama-c。

我正在从事这个项目，我需要找到以下理论证明。

我有一种特殊类型的二叉树，其中

1）每个内部节点肯定会有两个孩子。

2）有n个叶子节点，可以假设从最左边到最右边从1到n的顺序。

现在很明显，具有这两个属性的这种可能的树将呈指数级增长。

如果我从任何随机树开始并随机采样其中一个内部节点，请随机执行左旋转或右旋转（https://en.wikipedia.org/wiki/Tree_rotation）这两个操作之一。是否可以从任何随机树开始到搜索空间中的任何其他树。

我尝试了各种资源，但找不到任何证据。我自己尝试过，但无法找到解决方案。如果有人可以在这里帮助我，我会很高兴。