Как я могу сказать Дафни, что метод всегда возвращает объект `new`? - PullRequest
Новая
       5

Как я могу сказать Дафни, что метод всегда возвращает объект `new`?

0 голосов
/ 10 мая 2018

В этом примере , у меня есть метод, который возвращает новый массив: 

method Zeroes(len: nat) returns (h: array<nat>)
  ensures h.Length == len && all_zeroes(h)
{
  h := new nat[len];
  ...
}

и другой метод, который пытается его использовать: 

method Histogram(a: array<nat>, limit: nat) returns (h: array<nat>)
  requires greater_than_all(limit, a)
  ensures h.Length == limit && histogram_of(h, a)
{
  h := Zeroes(limit);
  assert histogram_of_prefix(h, a, 0);

  var i := 0;
  while i < a.Length
    invariant 0 <= i <= a.Length
    invariant histogram_of_prefix(h, a, i)
  {
    var n := a[i];
    h[n] := h[n] + 1;
    i := i + 1;
  }
}

Дафни жалуется, потому что не может доказать, что Zeroes(limit) не вернется a. (Если это когда-нибудь произойдет, мой код будет полностью сломан, справедливо отмечает Дафни.)

Похоже, что из функции Zeroes в функцию я забрал некоторую информацию. Если я переместлю тело Zeroes обратно в Histogram, то Дафни увидит h := new nat[limit];, что знает, что это не тот же массив, что и a, и проверка пройдет успешно.

Как я могу изменить подпись Zeroes, чтобы сообщить Дафни, что он всегда возвращает новый массив?

1 Ответ

0 голосов
/ 10 мая 2018

Вы можете использовать fresh для этого.Как и в 

ensures fresh(h)

См. Также этот вопрос .

...