如何在 Dafny 中将一个值转换为两个字节？

【问题标题】：How can I cast a value into two bytes in Dafny?如何在 Dafny 中将一个值转换为两个字节？
【发布时间】：2019-05-13 15:30:24
【问题描述】：

我想将一个整数从 0 转换为 65355，为此我需要一个两字节表示。我试图将它除以 2、8 倍，并在其余部分为 1 时将 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];
}

【问题讨论】：

标签： dafny

【解决方案1】：

要完成您的示例，您需要更强大的循环不变量。但是你根本不需要循环，因为没有理由只除以 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;
}

鲁斯坦

【讨论】：

谢谢你，鲁斯坦！我把整个事情复杂化了。