Дафни: типы с ограничениями

Я пробую кое-что в Дафни. Я хочу закодировать простую структуру данных, которая хранит несжатое изображение в памяти:

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): ошибка: неверный тип аргумента конструктора типа данных (найдена последовательность, ожидаемый массив) 1 ошибка разрешения/типа обнаружена в stdin.dfy

Я также мог бы потребовать, чтобы массив байтов не был нулевым, а размер массива байтов был равен ширине * высоте * 3 (для хранения трех байтов, представляющих значение RGB этого пикселя).

Каким образом я должен обеспечить это? Я изучил newtype, который позволяет накладывать некоторые ограничения на переменные определенного типа, но это работает только для числовых типов.


dafny
person Ruben    schedule 16.02.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

Поскольку полуоткрытые интервалы преобладают в информатике, синтаксис Дафни благоприятствует им. Например, для последовательности s выражение s[52..57] обозначает подпоследовательность s длины 5 (то есть 57 минус 52), начинающуюся в s с индексом 52. Еще одна вещь: вы также можете исключить тип int из b, если вы хочу, так как Дафни сделает вывод:

newtype byte = b | 0 <= b < 256

Вы также спрашивали о возможности добавления ограничения типа, чтобы последовательность в вашем типе данных всегда имела длину 3. Как вы обнаружили, вы не можете сделать это с newtype, потому что newtype (по крайней мере, на данный момент) работает только с числовыми типы. Однако вы можете (почти) использовать тип подмножества. Это будет сделано следующим образом:

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

(В этом примере первая вертикальная черта похожа на ту, что указана в объявлении newtype, и говорит «такой, что», тогда как следующие две обозначают оператор длины для последовательностей.) Проблема с этим объявлением в том, что типы должны быть непустыми, а Dafny не уверен, что существуют значения, удовлетворяющие ограничению triple. Что ж, Дафни не очень старается. План состоит в том, чтобы добавить предложение witness к объявлению type (и newtype), чтобы программист мог показать Дафни значение, принадлежащее типу triple. Однако эта поддержка ожидает некоторых изменений реализации, которые позволят настраивать начальные значения, поэтому в настоящее время вы не можете использовать это ограничение.

Не то чтобы вы хотели этого здесь, но Дафни позволил бы вам указать более слабое ограничение, допускающее пустую последовательность:

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

Итак, вместо этого, если вы хотите рассказать о том, что значение image имеет компонент data длины 3, тогда введите предикат:

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

и используйте этот предикат в спецификациях, таких как предварительные и постусловия.

Программируйте безопасно,

Рустан

person Rustan Leino    schedule 28.02.2017