выражение свойств индуктивных типов данных в Dafny

Я определил тип данных сигма-алгебры в 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
    }
}

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

Вот пример того, что я пробовал:

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.

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


properties algebraic-data-types quantifiers dafny
person Watermelon    schedule 23.03.2020    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Тип — это не то же самое, что набор в Дафни. Вы хотите выразить кванторы в своих леммах следующим образом:

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)

Рустан

person Rustan Leino    schedule 24.03.2020