Создание массива типа класса в dafny - PullRequest
Новая
       26

Создание массива типа класса в dafny

0 голосов
/ 10 ноября 2019

У меня проблема с созданием массива объектов типа класса, который я создал в dafny. Проблема заключается в том, что при инициализации нового массива этого типа я получаю эту ошибку в vscode:

, если не предусмотрен инициализатор для элементов массива, новый массив 'Cup' должен иметь пустой размер

Это код (фактически урезанная версия, которая все еще иллюстрирует проблему): 

datatype Drink = WATER | LEMONADE | COFFEE | TEA

class Cup {
  var volume: int
  var drink_type: Drink
  var dirty: bool

  predicate Valid()
  reads this;
  {
    volume >= 0 
  }

  constructor (v: int, dt: Drink, d: bool)
  requires v >= 0;
  ensures Valid();
  {
    volume := v;
    drink_type := dt;
    dirty := d;
  }
}

method FilterCupDrinkType(a: array<Cup>, dt: Drink) returns (b: array<Cup>, n: int)
{
  var temp := new Cup[a.Length]; 
}

Я просмотрел руководство и онлайн, но не смог найти ответтак что я надеюсь, что кто-то здесь знает, что делать. Если это невозможно сделать в dafny (очень плохо знаком с dafny), я был бы признателен за любые предложения по проверке чего-то подобного. Спасибо!

1 Ответ

0 голосов
/ 11 ноября 2019

Вы можете создать значение по умолчанию Cup и затем инициализировать массив следующим образом: 

method FilterCupDrinkType(a: array<Cup>, dt: Drink) returns (b: array<Cup>, n: int)
{
  var default := new Cup(0, WATER, false);
  var temp := new Cup[a.Length](_ => default); 
}

, или вы можете разрешить temp быть массивом, допускающим значение NULL Cup s (т. Е. Cup?) 

method FilterCupDrinkType(a: array<Cup>, dt: Drink) returns (b: array<Cup>, n: int)
{
  var temp := new Cup?[a.Length]; 
}

или вы можете скопировать a следующим образом 

method FilterCupDrinkType(a: array<Cup>, dt: Drink) returns (b: array<Cup>, n: int)
{
  var temp := new Cup[a.Length](i requires 0 <= i < a.Length reads a => a[i]); 
}

Часто хороший способ найти решение для таких вопросов, если вы не хотите ждатьответ здесь - поиск по обширному набору тестов Дафни по адресу https://github.com/dafny-lang/dafny/tree/master/Test. Конечно, учебник - лучший выбор, если рассматривать тему.

...