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

问题描述

在创建我在dafny中创建的类类型的对象数组时遇到问题。问题是初始化该类型的新数组时，我在vscode中遇到此错误：

I'm having a problem with creating an array of objects of a class type I created in dafny. The problem is when initialising a new array of that type I'm getting this error in vscode:

除非为该数组提供了初始化程序元素，则新的杯子数组必须为空大小

unless an initializer is provided for the array elements, a new array of 'Cup' must have empty size

这是代码（实际上是剥离后的版本，仍然说明了问题）：

This is the code (actually a stripped back version that still illustrates the problem):

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的新手），我将对验证此类建议提供任何建议。谢谢！

I looked through the manual and online but couldn't really find an answer so I'm hoping someone here knows what to do. If its not possible to do this in dafny(very new to dafny) I would appreciate any suggestions on verifying something like this. Thanks!

推荐答案

您可以创建默认的杯子，然后初始化数组如下所示

You could create a default Cup and then initialize the array with it as follows

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 s的数组（即 Cup？）

or you could allow temp to be an array of nullable Cups (i.e., 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上搜索Dafny广泛的测试套件。 ：//github.com/dafny-lang/dafny/tree/master/Test 。当然，如果处理该主题，则教程是一个更好的选择。

Often a good way to find solutions for such questions, if you don't want to wait for an answer here, is to search through Dafny's extensive test suite at https://github.com/dafny-lang/dafny/tree/master/Test. Of course the tutorial is a better choice if treats the topic.

这篇关于在dafny中创建类类型的数组的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！