在dafny中创建一个类型的数组[英] Creating an array of a class type in dafny

问题描述

我在创建我在 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 来说非常新)，我将不胜感激有关验证此类内容的任何建议.谢谢！

推荐答案

你可以创建一个默认的 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 是一个可以为空的 Cup 数组(即 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.当然，如果处理主题，教程是一个更好的选择.

本文地址：https://www.itbaoku.cn/post/1793866.html