свойства индуктивных типов данных в Дафни - PullRequest
Новая
       68

свойства индуктивных типов данных в Дафни

0 голосов
/ 24 марта 2020

Я определил тип данных сигма-алгебры в Dafny, как показано ниже: 

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg) | Set(s: set<int>)

class test {

    var S : set<int>

    function eval(X: Alg) : set<int>  // evaluates an algebra
        reads this;
        decreases X;
    {
        match X
        case Empty => {}
        case Complement(a) => S - eval(X.a)
        case Union(b,c) => eval(X.b) + eval(X.c)
        case Set(s) => X.s
    }
}

Я хочу указать свойства, определяемые количественно по индуктивному типу данных. Можно ли express свойств, как это?

Вот пример того, что я пытался: 

lemma algebra()
    ensures exists x :: x in Alg ==> eval(x) == {};
    ensures forall x :: x in Alg ==> eval(x) <= S;
    ensures forall x :: x in Alg ==> exists y :: y in Alg && eval(y) == S - eval(x);
    ensures forall b,c :: b in Alg && c in Alg ==> exists d :: d in Alg && eval(d) == eval(b) + eval(c);

Но я получаю сообщение об ошибке:

Второй аргумент «in» должен быть множеством, мультимножеством или последовательностью с элементами типа Alg или картой с доменом Alg

Я хочу указать такие свойства как: « there существует такая алгебра, что ..."или" для всех алгебр ...".

1 Ответ

1 голос
/ 24 марта 2020

Тип не совпадает с набором в Дафни. Вы хотите express квантификаторы в своих леммах следующим образом: 

lemma algebra()
  ensures exists x: Alg :: eval(x) == {}
  ensures forall x: Alg :: eval(x) <= S
  ensures forall x: Alg :: exists y: Alg :: eval(y) == S - eval(x)
  ensures forall b: Alg, c: Alg :: exists d: Alg :: eval(d) == eval(b) + eval(c)

Таким же образом вы можете объявить переменную x для типа int, но вы не пишете x in int.

Из-за вывода типа вам не нужно явно писать : Alg. Вы можете просто написать: 

lemma algebra()
  ensures exists x :: eval(x) == {}
  ensures forall x :: eval(x) <= S
  ensures forall x :: exists y :: eval(y) == S - eval(x)
  ensures forall b, c :: exists d :: eval(d) == eval(b) + eval(c)

Еще один комментарий к примеру: здесь вы определяете математику. Когда вы это делаете, обычно неплохо держаться подальше от императивных функций, таких как классы, методы и изменяемые поля. Вам не нужны такие функции, и они просто усложняют математику. Вместо этого я предлагаю удалить класс, изменив объявление S на const и удалив предложение reads. Это дает вам: 

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg) | Set(s: set<int>)

const S: set<int>

function eval(X: Alg): set<int>  // evaluates an algebra
  decreases X
{
  match X
  case Empty => {}
  case Complement(a) => S - eval(X.a)
  case Union(b,c) => eval(X.b) + eval(X.c)
  case Set(s) => X.s
}

lemma algebra()
  ensures exists x :: eval(x) == {}
  ensures forall x :: eval(x) <= S
  ensures forall x :: exists y :: eval(y) == S - eval(x)
  ensures forall b, c :: exists d :: eval(d) == eval(b) + eval(c)

Растан

...