问题标签 [formal-verification]

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

这是函数的主体：

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

如何比较两个 LTL 以查看其中一个是否相互矛盾？我问这个是因为我有一个分层状态机和描述每个状态行为的 LTL。我需要知道本地 LTL 是否可以与全局 LTL 相矛盾。我在文章“特征规范和自动冲突检测”中看到，如果 L(f) 交集 L(g) 为空，则两个 LTL 属性 f 和 g 不一致。这正是以 f 作为程序和 ¬g 作为属性的模型检查问题。谁能帮我这个？如何将 LTL f 转换为 SPIN/Promela 中的程序？

谢谢。

我正在为将给定字符串附加到动态字符数组末尾的函数编写 ACSL 规范。

这是我到目前为止所拥有的：

因为还不支持动态内存分配的验证，所以我添加了一个占位符函数char_vector_reallocate()和 ACSL 规范，但没有展示实现。

使用 Frama-C Sodium-20150201 和 WP 插件，我无法验证 6 个属性：

• typed_char_vector_append_disjoint_ok_err
• typed_char_vector_append_err_post
• typed_char_vector_append_err_post_length_unchanged
• typed_char_vector_append_ok_post
• typed_char_vector_append_ok_post_str_length_added_to_length
• typed_char_vector_append_ok_post_string_appended

我没想到验证前 5 个属性会遇到任何困难。

如何修复 ACSL 以便char_vector_append()验证？

（作为旁注，是否有我可以参考的动态数组的示例 ACSL 规范？）

我目前正在 Z3 之上为我的编程语言编写一个自动验证器，作为一个有趣的项目，我试图用它来证明使用循环的斐波那契实现等同于递归。

如果输入程序正确，它似乎可以工作，即它为 Z3 生成合理的输入，而 Z3 说它不能满足，这意味着在我的上下文中，程序是正确的。但是当我更改了一个变量初始化并因此导致程序不正确时，我的验证器提出了以下 Z3 公式，这对我来说似乎并不太复杂，但 Z3 说“未知”。

请注意，这两个量词表示斐波那契的递归定义。我的一个朋友告诉我这个技巧来避免匹配循环：我没有将 fib 定义为递归函数，而是引入了另一个我没有提供定义的函数 fakeFib，我在 fib 的递归定义中使用了该函数。另外，我告诉验证者它们是相等的，但是量词只得到 fib 的模式，而不是 fakeFib 的模式。由于模式的限制，它是不完整的，即，它只能证明程序的正确性，只要看一层递归就足以证明它（但它可以很容易地扩展到 k 层）。但我可以忍受这个限制，以避免匹配循环。

代码的“错误”是我错误地初始化了一个变量，这最终导致(= 1 (fib 0))最后一个断言中的组件不正确。对于正确的程序，它将是(= 0 (fib 0)).

一些观察：

• 如果我替换(= 1 (fib 0))为(= 0 (fib 0))，那么 Z3 立即发现它无法满足。
• 以前，我没有选项(set-option :smt.auto-config false)和(set-option :smt.mbqi false)设置，然后它在我的机器上耗尽内存并且在rise4fun 上超时。
• 似乎对有类似问题的人有用的设置(set-option :smt.macro-finder true)对我不起作用。我猜这是因为我有两个量词，fib而不仅仅是一个。
• 我尝试使用 cvc4 作为比较，它立即说“未知”。所以我的问题似乎不是 Z3 特有的。
• 该公式显然是可满足的。(= 1 (fib 0))是false，因此整个最后一个断言自动为真。(>= n 0)也很容易满足。

进程 a 或进程 b 进入临界区，但不是同时。如果发生这种情况（即它们同时进入临界区），将执行中断。

p = 进程 a

q = 进程 b

r = 临界区

运算符 ∨ = 或

运算符 → = 蕴涵

我的答案 ：

(p ∨ q) → r

这是正确的还是我做错了什么？我试图理解命题逻辑。

我正在研究为 java.util.PriorityQueue.remove(Object object) 方法创建 JML 规范。到目前为止，我已经想到了以下前提：

我现在正试图找出后置条件。那么这个方法的 Ensure 字段是什么？我觉得它应该涉及 size() 方法并确保数据不再在队列中，但我不确定如何编写。

我尝试在 dafny 中编写一个递归求和函数并证明其正确性。我已经写了：

这是我写的证明：

总和1：

总和2：

我得到的错误：

请帮我理解为什么？

我在下面的链接中为代码编写了以下证明。我想在证明 count2 方法方面获得一些帮助。交替证明对我来说不是很清楚，谢谢

http://rise4fun.com/Dafny/ueBY

2 个问题 -

1. 在基于断言的形式验证中，如果我得到一个不确定的断言，那么处理该断言或收敛它的各种方法是什么？
2. 开发参考 rtl 并编写断言来比较参考 rtl 输出与每个有效时钟沿上的 DUT 输出是否是正确的方法？它会增加有效的状态空间并因此增加复杂性和运行时间吗？

如果有人可以为基于断言的形式验证提供一些很好的参考材料，这也会很有帮助，因为我找不到太多关于这个主题的文章/论文。

我试图在 dafny 中证明这个程序，但我仍然得到最后一个不变量的错误，我不明白为什么它不起作用。

该程序包含一个将 int 插入排序数组的方法。int 将插入正确的位置，即：将 5 插入 1,2,3,4,5,6,7 将返回：1,2,3,4,5,5,6,7

谢谢