Я хочу преобразовать целое число от 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];
}
Чтобы завершить ваш пример, вам нужны более сильные инварианты цикла. Но вам вообще не нужен цикл, так как нет смысла делить только на 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;
}
Рустан
Спасибо, Рустан! Я все усложнял.