标签: formal-verification

我希望能够将一个大型测试分成较小的测试,以便当较小的测试通过时,它们意味着大测试也会通过(因此没有理由进行原始的大测试).我想这样做,因为较小的测试通常花费更少的时间,更少的努力和更少的脆弱.我想知道是否有测试设计模式或验证工具可以帮助我以稳健的方式实现这个测试分裂.

我担心当有人在一组较小的测试中改变某些东西时,较小的测试和原始测试之间的连接就会丢失.另一个担心是,一组较小的测试并没有真正涵盖大考验.

我的目标是一个例子:

//Class under test
class A {

  public void setB(B b){ this.b = b; }

  public Output process(Input i){
    return b.process(doMyProcessing(i));
  }

  private InputFromA doMyProcessing(Input i){ ..  }

  ..

}

//Another class under test
class B {

   public Output process(InputFromA i){ .. }

  ..

}

//The Big Test
@Test
public void theBigTest(){
 A systemUnderTest = createSystemUnderTest(); // <-- expect that this is expensive

 Input i = createInput();

 Output o = systemUnderTest.process(i); // <-- .. or expect that this …

是否有一个工具可以处理模型检查大型,真实世界,主要是C++,分布式系统,如KDE？

(KDE是一个分布式系统,因为它使用IPC,虽然通常所有进程都在同一台机器上.顺便说一下,这是"分布式系统"的有效用法 - 检查维基百科.)

该工具需要能够处理进程内事件和进程间消息.

(假设如果该工具支持C++,但不支持KDE使用的其他东西,如moc,我们可以一起破解某些东西以解决这个问题.)

我很乐意接受不太通用(例如专门用于查找特定类型的错误的静态分析器)或更一般的静态分析替代方案,而不是实际的模型检查器.但我只对能够实际处理KDE大小和复杂性项目的工具感兴趣.

我想在 Z3 中对固定大小的内存缓冲区及其访问操作进行建模。缓冲区的大小可以从几个字节到数百个字节不等。几个现有工具（例如，KLEE）采用的标准方法是在位向量的域和范围内创建数组变量。每个内存缓冲区都会获得这样一个数组，并且内存读/写使用select/store操作进行编码。

唉，在我的基准测试中，使用这种方法时，Z3(*) 似乎始终比 STP 慢。在更详细地分析查询以弄清楚发生了什么之前，我想确保我使用了“正确”的方法来编码 Z3 中的内存操作（因为，无可否认，STP 专门设计用于数组和位向量）。

那么在 Z3 中表示内存缓冲区的最有效方法是什么？到目前为止，我正在考虑几个替代方案：

1. 使用断言来指定内存缓冲区的初始值，而不是使用嵌套的store-s。然而，在我的初步测试中，这似乎更能减慢 Z3 的速度。
2. 使用位向量对缓冲区进行编码。但是，生成的位向量可能会变得非常大（约 1000 位），我不确定 Z3 或任何其他求解器是否可以有效地处理它。
3. 为每个内存字节创建单独的位向量变量，并使用嵌套ite表达式将内存访问路由到相应的变量。但是，我担心这会使模型复杂化并引入对量词的需求。
4. 使用未解释的函数而不是数组，但这需要以可能比 Z3 自己的内置数组理论效率低的方式重新定义数组公理。

有没有更好的方法我错过了？

(*) 默认非增量求解器，Z3 分支 unstable@aba79802cfb5

我(错误地)选择了关于验证并发程序的课程,到目前为止我们已经介绍了这种称为"Owicki-Gries方法"的方法.显然,通过将断言与每个语句相关联,可以证明关于程序的各种结果,并且显示这些断言是归纳的并且不会相互干扰.我们的任务之一涉及Lamports的快速互斥算法,详见本文:

在论文中,给出了Owicki-Gries风格的互斥证明.它看起来完全反直觉.我很难理解的是如何首先提出这些断言？你何时知道这些断言既不是太强大(如此强大以至于它打破了干扰自由),也不是太弱(例如一些微不足道的东西,比如每个陈述的重言式)？

干杯

对于学习依赖类型,我正在重写伊德里斯的旧Haskell游戏.目前游戏"引擎"使用内置整数类型,例如Word8.我想证明一些涉及这些数字的数值属性的引理(例如,双重否定是同一性).但是,不可能对原始算术运算的行为说些什么.会是什么更好的,只使用believe_me或其他handwaving(至少在最基本的属性),或者重写使用我的代码Nat,Fin和其他"高层"数值类型？

我想在一些可能被称为完全声明的Horn逻辑(或完全声明的Prolog)中形式化一些知识并执行查询.任何人都可以提供一些如何实施它的指导方针吗？我简要回顾一下上面链接中的精细描述:

形式语言是Prolog的核心语言:"程序"是Prolog中的一组规则和事实(包括函数和变量,基本上只包含用户定义的谓词).

然而,与Prolog相比,我正在寻找一种完整的逻辑程序标准声明语义 - 最少Herbrand模型(即归纳定义的基础术语集).在逻辑编程的理论工作中,这通常是研究的对象,众所周知,可以获得对查询的完整和完整的答案(在"递归可枚举的"意义上),例如,使用SLD解析以下条件:

• 公平搜索匹配规则(例如,Prolog的深度优先搜索不公平);
• 与" 发生检查 " 统一(检查变量在与其统一的术语中不会发生).

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

我的意图是以完全陈述的方式形式化一些知识.这种形式化的关键特征是它精确地对应于(单调)归纳的数学概念,因此可以通过归纳论证容易地推理知识及其属性.

我正在学习精益教程的第 4 章。

我希望能够证明简单的等式，例如a = b ? a + 1 = b + 1 无需使用 calc 环境。换句话说，我想明确构建以下证明项：

example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry

我最好的猜测是我需要使用eq.subst标准库中关于自然数相等的一些相关引理，但我不知所措。我能找到的最接近的精益例子是这样的：

example (A : Type) (a b : A) (P : A ? Prop) (H1 : a = b) (H2 : P a) : P b := eq.subst H1 H2

优化编译器的最终目的是在程序空间中搜索与原始程序等效但速度更快的程序。这已在实践中针对非常小的基本块完成：https : //en.wikipedia.org/wiki/Superoptimization

听起来困难的部分是搜索空间的指数性质，但实际上并非如此；困难的部分是，假设你找到了你正在寻找的东西，你如何证明新的、更快的程序真的等同于原始程序？

上次我研究它时，在证明某些上下文中程序的某些属性方面取得了一些进展，特别是在讨论标量变量或小的固定位向量时在很小的范围内，但在证明程序的等效性方面并没有真正取得进展当您谈论复杂的数据结构时，规模更大。

有没有人想出一种方法来做到这一点，甚至“模解决这个我们还不知道如何解决的 NP 难搜索问题”？

编辑：是的，我们都知道停机问题。它是根据一般情况定义的。人类是一个存在证明，这可以用于许多感兴趣的实际案例。

在尝试证明某些事情时，我遇到了一个无辜的声称，即我未能在Coq中证明。有人声称，对于给定的有限合奏，幂集也是有限的。该声明在下面的Coq代码中给出。

我浏览了关于有限集的Coq文档以及关于有限集和幂集的事实，但是我找不到将幂集解构为子集的并集的东西（以便Union_is_finite可以使用构造函数）。另一种方法可能是显示幂集的基数为2 ^ | S |。但是在这里我当然不知道如何处理证明。

From Coq Require Export Sets.Ensembles.
From Coq Require Export Sets.Powerset.
From Coq Require Export Sets.Finite_sets.

Lemma powerset_finite {T} (S : Ensemble T) :
  Finite T S -> Finite (Ensemble T) (Power_set T S).
Proof.
  (* I don't know how to proceed. *)
Admitted.

我有两个打包的信号数组,我需要为该属性创建一个属性和相关的断言,证明这两个数组在某些条件下是相同的.我正式验证并且该工具无法在单个属性中证明两个完整数组,因此我需要将其拆分为单个元素.那么有没有办法可以使用循环为数组的每个元素生成属性？目前,我的代码非常冗长,难以导航.

我的代码目前看起来像这样:

...
property bb_3_4_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][4] == bb_rtl [3][4] ;
endproperty

property bb_3_5_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][5] == bb_rtl [3][5] ;
endproperty

property bb_3_6_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][6] == bb_rtl [3][6] ;
endproperty
...

...
assert_bb_3_4: assert property (bb_3_4_p);
assert_bb_3_5: assert property (bb_3_5_p);
assert_bb_3_6: assert property (bb_3_6_p);
...

这就像我希望我的代码看起来像:

for (int i = 0; i < 8; i++) 
  for (int j = 0; j < 8; j++) 
  begin   
     property bb_[i]_[j]_p;
        @(posedge …