Dafny 无法证明函数方法等价，高阶多态递归与线性迭代
这个消息会有点长，但那是因为我想尽可能地解释它. 在 Dafny 中，我遇到了下一个问题:给定一个数组，计算发生这种情况的长度为 k 的段的数量；片段左半部分的正数大于或等于右半部分. 作为一个例子(想象段只能是偶数，所以没有讨论半是什么): k=2 --->计数(数组[-4,-2,2,1],k)--->2，因为 [-4,-2] 满足并且 [2,1]k=4 --->计数(数组[-4,
..
formal-verification相关内容
Dafny 无法证明函数方法等价，高阶多态递归 vs 线性迭代
这个消息会有点长，但那是因为我想尽可能地解释它. 在 Dafny 中，我遇到了下一个问题:给定一个数组，计算发生这种情况的长度为 k 的段的数量；片段左半部分的阳性数大于或等于右半部分. 举个例子(想象段只能是偶数，所以没有关于一半是什么的讨论): k=2 --->计数(数组 [-4,-2,2,1],k)--->2，因为 [-4,-2] 满足并且 [2,1]k=4--->计数(数组
..
Dafny和发生次数计数
我一直在研究Dafny中的引理的用法，但发现很难理解，显然以下示例无法验证，很可能是因为Dafny没有看到归纳法或诸如引理之类的证明计数属性?基本上，我不知道我该如何定义或需要定义什么来帮助说服Dafny计数是归纳的，等等.一些保证和不变性规范不是必需的，但这不是重点.顺便说一句，这在Spec#中更容易. 功能计数(项:seq
..
Coq VST内部结构复制
针对Coq 8.10.1的VST(已验证软件工具链)2.5v库遇到问题: 使用VST的最新工作提交时出错，即"不支持内部结构复制".最小的例子: struct foo {unsigned int a;};struct foo f(){struct foo q;返回q;} 在启动证明时出现错误: 错误:策略失败:(_q)％expr表达式包含内部结构复制，这是可验证C(级别97)当
..
从包容到精益中的平等
给出集合包含及其相反的证明，我希望能够证明两个集合相等. 例如，我知道如何证明以下语句，然后与此相反: open set universe u variable elem_type : Type u variable A : set elem_type variable B : set elem_type def set_deMorgan_incl : A ∩ B ⊆ set.co
..
在Coq中提供示例，其中(A B:Prop)，P:Prop->键入，以使A<-> B，但不能用P B代替P A
按照标题的要求，我希望举一个例子: Section Question: Definition A: Prop := . Definition B:Prop := . Definition/Inductive/Fixpoint P: Prop -> Type := . Theor
..
具有自定义理论的SMT求解器?
我正在做一些验证工作，在这些工作中我将常规树语法作为基础理论. Z3允许您使用未解释的函数来定义自己的东西，但是在您的决策过程是递归的时候，这往往无法正常工作.我认为他们曾经允许使用插件，但是已经过时了. 我想知道，有没有人建议过像样的SMT求解器，使您可以编写自定义理论的决策程序? 解决方案 鉴于最合理的SMT求解器是开源的，因此您有多种选择，您可以根据需要花费的时间和精力来
..
如何证明瘦= a = b→a + 1 = b + 1?
我正在研究精简教程的第4章. > 我希望能够证明简单的等式，例如a = b → a + 1 = b + 1 无需，而不必使用calc环境.换句话说，我想明确地构造以下证明项: example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry 我的最佳猜测是，我需要使用eq.subst和有关标准库中自然数相等的一些相关引理，但是我很茫
..
有没有办法证明程序没有错误?
我在考虑可以证明程序存在错误的事实.我们可以对其进行测试，以评估它或多或少具有抗虫性. 但是有没有办法(甚至从理论上)证明程序没有错误? 对于简单的程序，例如"Hello World"，我想我们应该可以做到. 但是大型程序呢? 解决方案 如今，有许多不同的形式主义可用于证明程序正确(例如，在证明助手中的形式化，依赖类型的编程语言，分隔逻辑，... ).正如其他人所指出的那样，没
..
在概念测试中，什么是“具体执行"?意思是?
当我经历 “所使用的方法建立在先前的工作之上，结合了象征性的执行和具体的执行，更具体地说，是使用这种组合来生成测试输入以探索所有可行的执行路径." 任何人都可以确认“具体执行"是什么意思吗?尽管进行了搜索，但我找不到任何直接的引文/明确的陈述. 据我了解，“具体执行"是指“以实际输入值执行程序，而不是符号执行，它假定变量，输入等具有符号值."如果我错了，请纠正我(如果可能，请举个小例
..
证明后继者对平等的替代性
我正在尝试从“精益定理证明"第7章中理解归纳类型. 我为自己设定了一个任务，以证明自然数的后继者具有对等式的替代属性: inductive natural : Type | zero : natural | succ : natural -> natural lemma succ_over_equality (a b : natural) (H : a = b) : (natur
..
如何比较两个零担?
如何比较两个LTL以查看一个LTL是否相互矛盾?我之所以这样问，是因为我有一个分层的状态机和描述每个状态行为的LTL.我需要知道本地LTL是否可以与全局LTL相矛盾.我在“功能规范和自动冲突检测"一文中看到，如果L(f)交集L(g)为空，则两个LTL属性f和g不一致.而这恰恰是模型检验问题，其中f为程序，¬g为属性.谁能帮我这个?如何将LTL f转换为SPIN/Promela中的程序? 谢谢
..
是否可以将一位的位向量转换为SMTLib2中的布尔变量?
我想要一个布尔变量，用于测试例如位向量的第三位是否为0.位向量理论允许提取1位作为位向量，但不能提取布尔类型.我想知道我是否可以做这个演员.谢谢. ===更新=== 很抱歉，我的问题不清楚.但是尼古拉·比约纳(Nikolaj Bjorner)的答案是如何测试位向量的某个位.虽然我想将位向量的第一位的值分配给一个变量.我尝试将示例修改如下: (declare-fun x () (_
..
在Z3中表示内存缓冲区的最有效方法
我想在Z3中为固定大小的内存缓冲区及其访问操作建模.缓冲区的大小可以从几个字节到数百个字节不等.几种现有工具(例如KLEE)使用的标准方法是在位向量的域和范围内创建数组变量.每个内存缓冲区都会得到一个这样的数组，并且使用select/store操作对内存的读/写进行编码. 可惜，在我的基准测试中，当使用这种方法时，Z3(*)似乎始终比STP慢.在更详细地分析查询以了解正在发生的事情之前，我想
..
Promela中的原子序列.文档矛盾
在这里 http://spinroot.com/spin/Man/Manual.html，上面写着: 在Promela中，还有另一种避免测试和设置的方法 问题:原子序列.通过为语句序列添加前缀 用大括号括起来并带有关键字atomic，用户可以指示 该序列将作为一个不可分割的单元执行， 不与任何其他过程交错. 它会导致运行时错误 如果除第一条语句外的任何语句阻塞了原子 顺序.这就是我们可以使用
..
在z3中打印内部求解器公式
定理证明工具z3花费大量时间来求解公式，我相信它应该能够轻松处理.为了更好地理解这一点并可能优化我对z3的输入，我想查看z3作为其求解过程的一部分生成的内部约束. 从命令行使用z3时，如何打印z3为其后端求解程序生成的公式? 解决方案 Z3命令行工具没有此类选项.此外，Z3包含几个求解器和预处理步骤.目前尚不清楚哪一步对您有用. Z3源代码可从 https://github.com/Z3P
..
ACSL后置条件中\ old的含义
我是Frama-C的新手用户，并且对断言有一些疑问 指针上方. 考虑以下涉及的C片段: 两个相关的数据结构Data and Handle，s.t.句柄有一个指向数据的指针； 数据中的“状态"字段，指示某些假设操作是否已完成 三个功能:init()，start_operation()和wait(); 使用上述方法的main()函数，其中包含6个断言(A1-A6) 现在，为什么
..
处理此数组的（数组）字段时，循环不变式不够强大
已更新 解决一些dafny问题的问题，下面将使用给定的类和相应的方法进行介绍。如果您需要其他东西，请告诉我，谢谢。链接也会使用rise4fun中的所有这些代码进行更新。 class TextEdit { var text：array
..
达夫尼：没有发现什么意思可以触发？
我在达夫尼（Dafny）得到警告，说我的量词有 未找到触发条件。 我要为代码执行的操作是找到平方值小于或等于给定自然数'n'的最大数字。这是到目前为止我想出的代码： 方法sqrt（n：nat）返回（r：int） //小于或等于n的平方 确保（r * r） （i * i）
..
指向旋转的2D矩形内部(不使用平移，触发函数或点积)
我想知道以下用于检查点是否在矩形内的算法是否有效. 我已经根据自己的直觉(没有足够的经验基础)来开发它，所以我很乐意听取对此事有更多经验的人的意见. 上下文: 该矩形定义有4个点.它可以旋转. 坐标始终是正数. 根据定义，如果该点与矩形相交，则视为该点. 假设: 使用点和矩形顶点之间的距离(下面的第一张图). 最大可能的总距离是该点位于一个顶点(第二张图)中. 如果
..