标签: formal-verification

Spark的新手,Ada的新手,所以这个问题可能过于宽泛.然而,作为尝试理解Spark的一部分,它是出于善意的要求.除了下面问题的直接答案,我欢迎对风格,工作流程等的批评.

作为我第一次涉足Spark,我选择尝试实现(简单)并证明正确性(迄今为止不成功)的功能 .

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

我从以下开始util.ads:

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);    
end Util;

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

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X/2 < 2**Floor_Log2'Result;
end Util;

有很多方法可以实现这个功能,我现在并不特别关注性能,所以我对它们中的任何一个都很满意.我认为"自然"实现(鉴于我的特定C背景)如下所示util.adb:

package body Util is
   function Floor_Log2 (X …

当我学习古兰经测试的概念时,我遇到了"具体和符号执行"这两个术语.(那里提到的文章,"CUTE:C的一个古老的单元测试引擎",在其摘要部分使用该术语.)

"所使用的方法建立在先前的工作基础上,结合了符号和具体执行,更具体地说,使用这样的组合来生成测试输入以探索所有可行的执行路径."

任何人都可以确认"具体执行"是什么意思吗？尽管我搜索,但我找不到任何直接引用/明确陈述.

根据我的理解,"具体执行"意味着"执行具有实际输入值的程序,而不像符号执行,它假定符号值为变量,输入等".如果我错了,请纠正我(如果可能的话,用一个小例子).

我试图从"精益证明中的证据"第7章中理解归纳类型.

我为自己设定了一个任务,证明自然数的继承者有平等的替代属性:

inductive natural : Type
| zero : natural
| succ : natural -> natural

lemma succ_over_equality (a b : natural) (H : a = b) :
  (natural.succ a) = (natural.succ b) := sorry

经过一些猜测和相当详尽的搜索后,我能够满足编译器的几种可能性:

lemma succ_over_equality (a b : natural) (H : a = b) :
  (natural.succ a) = (natural.succ b) :=
    eq.rec_on H (eq.refl (natural.succ a))
    --eq.rec_on H rfl
    --eq.subst H rfl
    --eq.subst H (eq.refl (natural.succ a))
    --congr_arg (? (n : natural), (natural.succ n)) H …

首先,这只能在没有副作用的算法上实现吗？

其次,我在哪里可以了解这个过程,任何好书,文章等？

定理证明工具z3花了很多时间来解决一个公式,我相信它应该能够轻松处理.为了更好地理解这一点并可能优化我对z3的输入,我想看到z3生成的内部约束作为其求解过程的一部分.当从命令行使用z3时,如何打印z3为其后端解算器生成的公式？

在阅读了大量论文之后,我试图找到CCured源(甚至是二进制文件)来尝试在我的C源代码中使用它.

但是,所有链接似乎都已死亡.经过一些谷歌搜索,我在这里问.有人可以上传它们(来源,文档等),如果你有任何机会在你的硬盘上有一个tarball吗？

编辑:我也通过电子邮件发送了一位作者,但还没有得到答复.稍后会尝试通过电子邮件发送给他人.

(引自论文)

构建了一个程序转换系统,为现有的C程序增加了类型安全保障.CCured尝试静态验证内存错误不会发生,并插入运行时检查静态验证不足.CCured通过根据用途分离指针类型来扩展C类型系统,它使用一种非常简单的类型推断算法推断现有C程序的适当指针种类.CCured使用物理子类型在编译时识别并验证大量类型转换.使用运行时类型信息验证其他类型转换.

Monadic一阶逻辑，其中所有谓词都恰好采用一个参数，是一阶逻辑的已知可判定片段。测试公式是否可以满足此逻辑是可以确定的，并且存在基于分辨率的方法来确定这一点。

我处于需要测试一些单子一阶逻辑语句的可满足性的情况。我意识到我将达到理论上的复杂性极限，但我希望在常见情况下能够获得合理的性能。

现在，存在大量的定理证明，它们提供了解决一阶逻辑问题的快速方法。其中包括Vampire，SPASS，E，以及Z3和CVC4的量词扩展。但是，由于不确定性，不能保证它们停止运行。

我的问题

在现有的定理证明者中，有谁能保证在给定单子式公式作为输入时停止？还是有一种方法可以使用它们（以某种方式）有效地测试单子公式的可满足性？

• 您使用了哪些类型的应用程序进行模型检查？
• 你使用什么模型检查工具？
• 您如何总结您使用该技术的经验,特别是在评估其提供更高质量软件的有效性方面？

在我学习的过程中,我有机会使用Spin,它引起了我对实际模型检查进行了多少以及组织从中获取多少价值的好奇心.在我的工作经历中,我从事过业务应用程序,其中(自然)没有考虑将正式验证应用于逻辑.我真的很想了解SO人员的模型检查经验和关于这个主题的想法.模型检查是否会成为我们工具箱中应该使用的更广泛使用的开发实践？

我一直在阅读关于形式验证的文章，基本点是它需要一个正式的规范和模型来使用。然而，许多来源将静态分析归类为形式验证技术，有些提到抽象解释并提到它在编译器中的使用。所以我很困惑 - 如果没有模型的正式描述，这些如何进行形式验证？
编辑：我发现的一个来源是：

静态分析：根据预定义的抽象（有时可以由用户自动/手动定制）从程序文本中自动计算抽象语义

那么这是否意味着它只适用于源代码而无需正式规范？这就是静态分析器所做的。

另外，在没有形式验证的情况下可以进行静态分析吗？例如，SonarQube 真的执行形式化方法吗？

我在想我们可以证明一个程序有错误.我们可以对其进行测试,以评估它是否或多或少具有抗虫性.

但有没有办法(甚至在理论上)证明程序没有错误？

对于简单的程序,例如"Hello World",我想我们应该能够做到.但是大型项目呢？