时间戳

首页 > 解决方案 > 如何在 Dafny 中将一个值转换为两个字节？

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

问题描述

我想将一个整数从 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

解决方案

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

鲁斯坦

推荐阅读