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

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

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

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?


dafny
person tjhance    schedule 06.05.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

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;

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

person James Wilcox    schedule 08.05.2018