Dafny: Typen mit Einschränkungen

Question

Ich versuche einige Dinge in Dafny. Ich möchte eine einfache Datenstruktur codieren, die ein unkomprimiertes Bild im Speicher hält:

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

Eigentlich ist es mit:

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 führt zu beklagen:

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

könnte ich möchte auch fordern Sie an, dass das Byte-Array nicht null ist, und die Größe des Byte-Arrays ist gleich width * height * 3 (um drei Bytes zu speichern, die den RGB-Wert dieses Pixels darstellen).

Wie soll ich dies durchsetzen? Ich habe in newtype gesucht, mit dem Sie einige Einschränkungen für Variablen mit einem bestimmten Typ festlegen können, aber dies funktioniert nur für numerische Typen.

Answer 1

Dafny unterstützt sowohl unveränderliche Sequenzen (die wie mathematische Sequenzen von Elementen sind) als auch veränderliche Arrays (die wie in C und Java Zeiger auf Elemente sind). Der Fehler, den Sie bekommen, sagt Ihnen, dass Sie den image Konstruktor mit einem seq<byte> Wert aufrufen, wobei ein array<byte> Wert erwartet wird.

Sie das Problem durch den Austausch Ihrer Definition von dat mit beheben können:

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

Allerdings, je mehr typische Sache, wenn Sie einen Datentyp verwenden (die unveränderlich ist), wäre eine Sequenz zu verwenden, . Also, wollen Sie wahrscheinlich stattdessen Ihre Definition von image ändern:

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

Btw

, beachten Sie, dass Dafny Sie das gleiche eine Art und eine seiner Erbauer nennen können, so gibt es keinen Grund, eine von ihnen zu nennen mit ein Prime (außer du willst natürlich).

Eine weitere Frage des Stils ist es, ein halboffene Intervall in Ihrer Definition von byte zu verwenden:

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

Seit halboffenen Intervalle in der Informatik, Dafny Syntax favorisiert sich weit verbreitet sind. Für eine Sequenz s zum Beispiel bezeichnet der Ausdruck s[52..57] eine Teilfolge von s der Länge 5 (also 57 minus 52) beginnend in s bei Index 52. Noch eine Sache, Sie können auch den Typ int von b auslassen, wenn Sie wollen, da Dafny es schließen wird:

immer,

newtype byte = b | 0 <= b < 256 

Sie auch über die Möglichkeit gebeten, eine Art Zwang des Hinzufügens, so dass die Sequenz in Ihrem Datentyp entdeckt 3. lang sein wird, wie Sie können Sie dies nicht mit a newtype, weil newtype (zumindest für jetzt) ​​nur mit numerischen Typen funktioniert. Sie können jedoch (fast) einen Teilmenge-Typ verwenden. Dies würde durchgeführt werden, wie folgt:

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

(. In diesem Beispiel ist die erste vertikale Stange ist, wie die in der newtype Erklärung und sagt „so dass“, während die nächsten zwei die Länge Operator auf Sequenzen bezeichnen) Das Problem mit dieser Deklaration ist, dass Typen nicht leer sein müssen und Dafny nicht davon überzeugt ist, dass es Werte gibt, die die Bedingung triple erfüllen.Nun, Dafny versucht nicht sehr hart. Der Plan ist, der (und newtype) -Deklaration eine witness-Klausel hinzuzufügen, sodass ein Programmierer Dafny einen Wert anzeigen kann, der zum triple-Typ gehört. Diese Unterstützung wartet jedoch auf einige Implementierungsänderungen, die benutzerdefinierte Anfangswerte ermöglichen, sodass Sie diese Einschränkung zu diesem Zeitpunkt nicht verwenden können.

Nicht, dass man es hier wollen, aber Dafny würde Sie eine schwächere Einschränkung geben, die die leere Sequenz gibt zu:

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

Anstatt also, wenn Sie, dass ein image Wert ein data hat sprechen will, Komponente der Länge 3, dann führen Sie ein Prädikat:

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

und verwenden Sie dieses Prädikat in Spezifikationen wie Pre-und Post-Bedingungen.

Programm sicher,

Rustan