Как написать чистую функцию в Дафни, чтобы получить минимум набора? - PullRequest
Новая
       60

Как написать чистую функцию в Дафни, чтобы получить минимум набора?

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

Я пытаюсь написать функцию, чтобы получить минимум непустого множества.

Вот что я придумал: 

method minimum(s: set<int>) returns (out: int)
requires |s| >= 1
ensures forall t : int :: t in s ==> out <= t
{
  var y :| y in s;
  if (|s| > 1) {
    var m := minimum(s - {y});
    out := (if y < m then y else m);
    assert forall t : int :: t in (s - {y}) ==> out <= t;
    assert out <= y;
  } else {
    assert |s| == 1;
    assert y in s;
    assert |s - {y}| == 0;
    assert s - {y} == {};
    assert s == {y};
    return y;
  }
}

Это неоптимально по двум причинам:

  • Дафни выдает «Не найдено условий для запуска». предупреждение за линию, 

    assert forall t : int :: t in (s - {y}) ==> out <= t;

    Однако удаление этой строки приводит к невозможности проверки кода. Насколько я понимаю, предупреждение о триггере не так уж плохо, это всего лишь предупреждение о том, что у Дафни могут возникнуть проблемы с линией. (Хотя, похоже, это действительно помогает.) Поэтому я чувствую, что делаю что-то неоптимальное или неидиоматическое.

  • Это довольно неэффективно. (Он каждый раз создает новый набор, так что это будет O (n ^ 2).) Но я не вижу другого способа перебора набора. Есть ли более быстрый способ сделать это? Действительно ли наборы предназначены для программирования «реального» не-призрачного кода в Dafny?

Итак, мой вопрос (в дополнение к вышесказанному): есть ли лучший способ написать функцию minimum?

1 Ответ

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

В этом случае я рекомендую игнорировать предупреждение о триггере, поскольку, похоже, оно работает нормально, несмотря на предупреждение. (Вывод триггера Дафни несколько чрезмерно консервативен, когда дело доходит до теоретических операторов множества, и Z3 может вывести хороший триггер на низком уровне.) Если вы действительно хотите это исправить, вот один из способов. Замените ветвь "then" вашего кода на 

var s' := (s - {y});
var m := minimum(s');
out := (if y < m then y else m);
assert forall t :: t in s ==> t == y || t in s';
assert forall t : int :: t in s' ==> out <= t;
assert out <= y;

Вторая проблема (об эффективности) является несколько фундаментальной. (См. Статью Растана «Компиляция оператора Эпсилона Гильберта» , где упоминается, что компиляция операторов «дай-так-то» приводит к квадратичной производительности.) Я предпочитаю думать о set Дафни как о математической конструкции, которая не должна быть скомпилированным. (Тот факт, что он может может быть скомпилирован, удобен для игрушечных программ, а не для реальных систем, где можно было бы ожидать реализации стандартных наборов библиотек, основанных на структуре данных.)

...