Как я могу привести значение в два байта в Дафни? - PullRequest
Новая
       8

Как я могу привести значение в два байта в Дафни?

0 голосов
/ 12 декабря 2018

Я хочу преобразовать целое число от 0 до 65355, и для этого мне нужно двухбайтовое представление.Я пытаюсь разделить его на 2, 8 раз, и суммировать степени 2, когда остальное равно единице, а затем привести это целое число как байт, но у меня возникают проблемы с соблюдением ограничений байта (256).Второй байт будет оставшимся от 8-го деления, и у меня возникают проблемы с преобразованием этого байта также.

Ниже приведен мой код для ранее описанного метода функции: 

method convertBin(i:int) returns (b:seq<byte>)
requires 0<=i<=65535;
{
  var b1:=0;
  var q:=i;
  var j:=0;
  while j<8
    invariant 0<=j<=8 && (b1 as int)< power(2,j)
    decreases 8-j
  {
    var p:int;
    if(q%2==1){
      p:=power(2, j);
      b1:=b1 + p;
      q:=q/2;
    }
    j:=j+1;
  }
  b1:=b1 as byte;
  b:=[b1]+[q as byte];
}

1 Ответ

0 голосов
/ 12 декабря 2018

Для завершения вашего примера вам нужны более сильные инварианты цикла.Но вам вообще не нужен цикл, так как нет никакой причины делить только на 2.

Здесь мы делаем это с byte как тип подмножества: 

type byte = x | 0 <= x < 256

method convertBin(i: int) returns (b1: byte, b0: byte)
  requires 0 <= i < 0x1_0000
  ensures i == 256 * b1 + b0
{
  b1, b0 := i / 256, i % 256;
}

И вотта же программа, но с byte, являющимся newtype: 

newtype byte = x | 0 <= x < 256

method convertBin(i: int) returns (b1: byte, b0: byte)
  requires 0 <= i < 0x1_0000
  ensures i == 256 * b1 as int + b0 as int
{
  b1, b0 := (i / 256) as byte, (i % 256) as byte;
}

Rustan

...