1

我在 Dafny 尝试一些东西。我想编写一个简单的数据结构，在内存中保存未压缩的图像：

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)：错误：数据类型构造函数参数的类型不正确（找到 seq，预期数组）在 stdin.dfy 中检测到 1 个分辨率/类型错误

我可能还想要求字节数组不为空，并且字节数组的大小等于宽度 * 高度 * 3（以存储表示该像素的 RGB 值的三个字节）。

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

4

1 回答 1

2

Dafny 支持不可变序列（类似于元素的数学序列）和可变数组（类似于 C 和 Java 中的元素指针）。您得到的错误是告诉您您正在使用预期值的值调用image构造函数。seq<byte>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]表示从索引 52s开始的长度为 5（即 57 减去 52）的子序列。另外，如果需要，您也可以省略类型，因为 Dafny 会推断它：sintb

newtype byte = b | 0 <= b < 256

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

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

（在本例中，第一个竖线与newtype声明中的竖线类似，表示“这样”，而接下来的两个竖线表示序列上的长度运算符。）这个声明的问题是类型必须是非空的，而 Dafny 不是t 确信存在满足 的约束的任何值triple。嗯，达芙妮不是很努力。计划是在(and ) 声明中添加一个witness子句，以便程序员可以向 Dafny 显示属于该类型的值。但是，此支持正在等待一些允许自定义初始值的实现更改，因此此时您不能使用此约束。typenewtypetriple

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

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

所以，相反，如果你想谈论一个image值有一个data长度为 3 的分量，那么引入一个谓词：

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

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

安全编程，

鲁斯坦

于 2017-02-28T02:24:18.047 回答