Блог

Dafny, похоже, не доказывает эквивалентность двух методов без постусловий. Ожидается ли это?

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;
}

 

Это ожидаемо. Dafny выполняет проверку «по одному методу за раз» и никогда не будет «заглядывать внутрь» кода другого метода.

Для получения дополнительной информации, пожалуйста, ознакомьтесь с этим разделом часто задаваемых вопросов, а также с разделом руководства под названием Утверждения (найдите «забыть», чтобы перейти к соответствующей части).