Dafny：有约束的类型

Question

我正在达夫尼尝试一些事情。我想编写一个简单的数据结构，在内存中保存未压缩的图像：

datatype image' = image(width: int, height: int, data: array<byte>)
newtype byte = b: int | 0 <= b <= 255

实际使用：

method Main() {
  var dat := [1,2,3];
  var im := image(1, 3, dat);
}

datatype image' = image(width: int, height: int, data: array<byte>)
newtype byte = b: int | 0 <= b <= 255

导致达芙妮抱怨：

stdin.dfy(3,24): Error: incorrect type of datatype constructor argument (found seq, expected array) 1 resolution/type errors detected in stdin.dfy

我可能还想要求字节数组不为空，字节数组的大小等于width * height * 3（存储三个字节代表该像素的RGB值）

我应该以什么方式执行此操作？我研究了 newtype，它允许您对具有特定类型的变量施加一些约束，但这仅适用于数字类型。

Answer 1

Dafny 支持不可变序列（类似于元素的数学序列）和可变数组（类似于 C 和 Java，指向元素的指针）。您得到的错误是告诉您您正在使用 seq<byte> 值调用 image 构造函数，而期望值是 array<byte>。

您可以通过将 dat 的定义替换为：

来解决此问题

var dat := new byte[3];
dat[0], dat[1], dat[2] := 1, 2, 3;

但是，如果您使用的是数据类型（不可变的），则更典型的做法是使用序列。因此，您可能希望将 image 的定义更改为：

datatype image = image(width: int, height: int, data: seq<byte>)

顺便说一句，请注意 Dafny 允许您将一个类型和它的构造函数之一命名为相同的名称，因此没有理由用素数命名其中一个（当然，除非您愿意）。

另一个风格问题是在 byte:

的定义中使用半开区间

newtype byte = b: int | 0 <= b < 256

由于半开区间在计算机科学中很普遍，因此 Dafny 的语法有利于它们。例如，对于序列 s，表达式 s[52..57] 表示 s 的子序列，长度为 5（即 57 减去 52），从 s 的索引 52 处开始。还有一件事，如果你愿意，你也可以省略 b 的 int 类型，因为 Dafny 会推断它：

newtype byte = b | 0 <= b < 256

您还询问了添加类型约束的可能性，以便您的数据类型中的序列长度始终为 3。正如您发现的那样，您不能使用 newtype 执行此操作，因为 newtype（至少现在）只适用于数字类型。但是，您（几乎）可以使用子集类型。这将按如下方式完成：

type triple = s: seq<byte> | |s| == 3

（在这个例子中，第一个竖线就像 newtype 声明中的竖线，表示 "such that"，而接下来的两个表示序列的长度运算符。）这个问题声明是类型必须是非空的，Dafny 不相信有任何值满足 triple 的约束。好吧，达夫尼并没有很努力。计划是向 type（和 newtype）声明添加一个 witness 子句，以便程序员可以向 Dafny 显示属于 triple 类型的值。但是，此支持正在等待一些允许自定义初始值的实现更改，因此此时您不能使用此约束。

这里不是你想要的，但 Dafny 会让你给出一个允许空序列的较弱约束：

type triple = s: seq<byte> | |s| <= 3

因此，相反，如果您想讨论 image 值具有长度为 3 的 data 分量，则引入谓词：

predicate GoodImage(img: image)
{
  |img.data| == 3
}

并在前置条件和后置条件等规范中使用此谓词。

安全编程，

鲁斯坦

Dafny：有约束的类型

Dafny: types with contraints

dafny