Эпсилон-оператор Гильберта

Для того чтобы оператор Гильберта эпсилон, также известный в Дафни как выражение пусть такой-то,

var z :| P; E

чтобы быть компилируемым, ограничение P должно однозначно определять z. В вашем случае ограничение P равно z in s, которое не определяет z однозначно, за исключением одноэлементных наборов.

Если бы s имел тип set<int>, вы могли бы (неэффективно) выполнить это требование, изменив свою функцию choose' на:

function method choose'<T>(s:set<int>):int
  requires s != {}
{
  var z :| z in s && forall y :: y in s ==> z <= y;
  z
}

Почти. Вам нужно убедить Дафни, что такой z существует. Вы можете сделать это в лемме. Вот работающая лемма, вероятно, длиннее, чем необходимо, но первое, что я получил, которая делает это. Обратите внимание, что в лемме также используется оператор Гильберта, но в контексте оператора, поэтому требование уникальности не применяется.

function method choose'<T>(s:set<int>):int
  requires s != {}
{
  HasMinimum(s);
  var z :| z in s && forall y :: y in s ==> z <= y;
  z
}

lemma HasMinimum(s: set<int>)
  requires s != {}
  ensures exists z :: z in s && forall y :: y in s ==> z <= y
{
  var z :| z in s;
  if s == {z} {
    // the mimimum of a singleton set is its only element
  } else if forall y :: y in s ==> z <= y {
    // we happened to pick the minimum of s
  } else {
    // s-{z} is a smaller, nonempty set and it has a minimum
    var s' := s - {z};
    HasMinimum(s');
    var z' :| z' in s' && forall y :: y in s' ==> z' <= y;
    // the minimum of s' is the same as the miminum of s
    forall y | y in s
      ensures z' <= y
    {
      if
      case y in s' =>
        assert z' <= y;  // because z' in minimum in s'
      case y == z =>
        var k :| k in s && k < z;  // because z is not minimum in s
        assert k in s';  // because k != z
    }
  }
}

К сожалению, тип вашего s не set<int>. Я не знаю, как получить уникальное значение из общего набора. :(

Информацию о важности требования уникальности в скомпилированных выражениях см. в этой статье.

Рустан

Хорошо, спасибо, я понимаю проблему компиляции не однозначно определенного значения. Однако, согласно вашему ответу, мой первый метод выбора должен вызывать ту же ошибку, что и метод выбора функции, не так ли?

method choose<T>(s:set<T>) returns (x:T)
	requires s != {}
{
var z :| z in s;
return z;
}

function choose'<T>(s:set<T>):T
// function method choose'<T>(s:set<T>):T // Activate this line and comment the previous line to see the error
	requires s != {}
{
var z :| z in s;
z
}