Dafny无法证明方法的等价性

Question

Dafny doens似乎不能证明没有后置条件的两种方法的等价性。这是意料之中的吗？

https://rise4fun.com/Dafny/c88u

function method pipeline_func(x: int): int{
    x * 2
}

function method program_func(x: int): int {
    x + x
}

method pipeline_with_ensures (x: int) returns (x': int) 
    ensures x' == x*2
{
    x' := x*2;
}

method program_with_ensures (x: int) returns (x': int) 
    ensures x' == x+x
{
    x' := x + x;
}

method pipeline(x: int) returns (x': int)
{
    x' := x * 2;
}

method program(x: int) returns (x': int)
{
    x' := x + x;
}

method Main(x: int) {
    // Simple functions can be directly called from expressions and can easily 
    // be asserted as below.
    assert pipeline_func(x) == program_func(x);

    // Methods needs to be assigned to a variables to be used in another
    // expression.
    var a := pipeline_with_ensures(x);
    var b := program_with_ensures(x);

    // With ensures in both program_with_ensures and pipeline_with_ensures 
    // Dafny can verify a equals to b. Similarly functions and methods could be 
    // asserted together. 
    assert a == b;
    assert a == pipeline_func(x);
    assert b == program_func(x);
    assert a == program_func(x);
    assert b == pipeline_func(x);

    var c := pipeline(x);
    var d := program(x);

    // However, without ensures clause, Dafny can't verify that pipeline and
    // pipeline_with_ensures actually compute the same thing. 
    assert a == c;

    assert c == d;
}

我在Dafny中有两个方法，我对他们的post条件没有太多的信息。这里的上下文是，我正在使用程序合成工具开发一个编译器，我想正式地验证我编译的程序对任意输入计算的值是否与规范中的值相同。我的规范是用类似C的语言编写的，如下所示。

#define ECN_THRESH 20

int counter   = ECN_THRESH;
int last_time = 0;

struct Packet {
  int bytes;
  int time;
  int mark;
};

void func(struct Packet p) {
  // Decrement counter according to drain rate
  counter = counter - (p.time - last_time);
  if (counter < 0) counter = 0;

  // Increment counter
  counter += p.bytes;

  // If we are above the ECN_THRESH, mark
  if (counter > ECN_THRESH) p.mark = 1;

  // Store last time
  last_time = p.time;
}

Answer 1

这是意料之中的。Dafny执行验证“一次一个方法”，并且永远不会“查看”另一个方法的代码。

有关更多信息，请参阅此FAQ section以及Guide中名为Assertions的部分(搜索"forget“可找到相关部分)。