Эпсилон-оператор Гильберта - PullRequest
Новая
       13

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

0 голосов
/ 06 июля 2018

Почему вы можете использовать эпсилон-оператор Гильберта в методе и в функции, но не в «методе функции»? 

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
}

Ответы [ 2 ]

0 голосов
/ 10 июля 2018

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

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
}
0 голосов
/ 10 июля 2018

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

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>. Я не знаю, как получить уникальное значение из общего набора. (

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

Rustan

...