Дафни не может доказать эквивалентность методов - PullRequest
Новая
       19

Дафни не может доказать эквивалентность методов

1 голос
/ 13 апреля 2019

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

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

У меня есть два метода в Дафни, которые у меня не так много информации о состоянии их должности.Здесь контекст заключается в том, что я разрабатываю компилятор с использованием инструмента синтеза программ, и я хотел бы официально проверить, что моя скомпилированная программа вычисляет то же значение, что и спецификация для любого произвольного ввода.Мои спецификации написаны на 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;
}

1 Ответ

0 голосов
/ 13 апреля 2019

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

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

...