Dafny：類型與contraints

Question

我想在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 

導致Dafny抱怨：

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中一樣，指向元素）。您收到的錯誤是告訴您，您正在調用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]表示長度爲5（即57減52）的s的子序列，其起始於索引52處的s。還有一件事，如果你有，也可以省略b的類型int希望，因爲Dafny會推斷出它：

newtype byte = b | 0 <= b < 256 

你還問有關添加類型約束的可能性，所以，在你的數據類型的順序永遠是長度3.當你發現，你不能做到這一點與一個newtype，因爲newtype（至少現在）只適用於數字類型。但是，您可以（幾乎）使用子集類型。這將如下進行：

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

（在這個例子中，第一垂直杆是像一個在newtype聲明並說「使得」，而接下來的兩個表示對序列的長度運算符）這個聲明的麻煩是類型必須是非空的，並且Dafny不相信有任何值滿足triple的限制。那麼，Dafny不是很努力。計劃是在type（和newtype）聲明中添加witness子句，以便程序員可以向Dafny顯示屬於triple類型的值。但是，此支持正在等待一些允許自定義初始值的實現更改，因此您目前無法使用此約束。

不是說你想在這裏，但Dafny將讓你給承認空序列的弱約束：

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

所以，相反，如果你想談論的image值具有data然後引入一個謂詞：

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

並在規則中使用此謂詞，如前置和後置條件。

程序安全，

Rustan